clasohm@1460: (* Title: tactic clasohm@0: ID: $Id$ clasohm@1460: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1991 University of Cambridge clasohm@0: clasohm@0: Tactics clasohm@0: *) clasohm@0: clasohm@0: signature TACTIC = paulson@1501: sig clasohm@0: val ares_tac: thm list -> int -> tactic clasohm@0: val asm_rewrite_goal_tac: nipkow@214: bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic clasohm@0: val assume_tac: int -> tactic clasohm@0: val atac: int ->tactic lcp@670: val bimatch_from_nets_tac: paulson@1501: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic clasohm@0: val bimatch_tac: (bool*thm)list -> int -> tactic lcp@670: val biresolve_from_nets_tac: paulson@1501: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic clasohm@0: val biresolve_tac: (bool*thm)list -> int -> tactic paulson@1501: val build_net: thm list -> (int*thm) Net.net paulson@1501: val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> paulson@1501: (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net clasohm@0: val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic clasohm@0: val compose_tac: (bool * thm * int) -> int -> tactic clasohm@0: val cut_facts_tac: thm list -> int -> tactic lcp@270: val cut_inst_tac: (string*string)list -> thm -> int -> tactic paulson@2029: val defer_tac : int -> tactic clasohm@0: val dmatch_tac: thm list -> int -> tactic clasohm@0: val dresolve_tac: thm list -> int -> tactic clasohm@0: val dres_inst_tac: (string*string)list -> thm -> int -> tactic clasohm@0: val dtac: thm -> int ->tactic clasohm@0: val etac: thm -> int ->tactic clasohm@0: val eq_assume_tac: int -> tactic clasohm@0: val ematch_tac: thm list -> int -> tactic clasohm@0: val eresolve_tac: thm list -> int -> tactic clasohm@0: val eres_inst_tac: (string*string)list -> thm -> int -> tactic clasohm@0: val filter_thms: (term*term->bool) -> int*term*thm list -> thm list clasohm@0: val filt_resolve_tac: thm list -> int -> int -> tactic clasohm@0: val flexflex_tac: tactic clasohm@0: val fold_goals_tac: thm list -> tactic clasohm@0: val fold_tac: thm list -> tactic clasohm@0: val forward_tac: thm list -> int -> tactic clasohm@0: val forw_inst_tac: (string*string)list -> thm -> int -> tactic paulson@2029: val freeze_thaw: thm -> thm * (thm -> thm) lcp@1077: val insert_tagged_brl: ('a*(bool*thm)) * paulson@1501: (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> paulson@1501: ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net paulson@1801: val delete_tagged_brl: (bool*thm) * paulson@1801: ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> paulson@1801: (int*(bool*thm))Net.net * (int*(bool*thm))Net.net clasohm@0: val is_fact: thm -> bool clasohm@0: val lessb: (bool * thm) * (bool * thm) -> bool clasohm@0: val lift_inst_rule: thm * int * (string*string)list * thm -> thm clasohm@0: val make_elim: thm -> thm paulson@1501: val match_from_net_tac: (int*thm) Net.net -> int -> tactic clasohm@0: val match_tac: thm list -> int -> tactic clasohm@0: val metacut_tac: thm -> int -> tactic clasohm@0: val net_bimatch_tac: (bool*thm) list -> int -> tactic clasohm@0: val net_biresolve_tac: (bool*thm) list -> int -> tactic clasohm@0: val net_match_tac: thm list -> int -> tactic clasohm@0: val net_resolve_tac: thm list -> int -> tactic clasohm@0: val PRIMITIVE: (thm -> thm) -> tactic clasohm@0: val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic clasohm@0: val prune_params_tac: tactic clasohm@0: val rename_tac: string -> int -> tactic clasohm@0: val rename_last_tac: string -> string list -> int -> tactic paulson@1501: val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic clasohm@0: val resolve_tac: thm list -> int -> tactic clasohm@0: val res_inst_tac: (string*string)list -> thm -> int -> tactic clasohm@0: val rewrite_goals_tac: thm list -> tactic clasohm@0: val rewrite_tac: thm list -> tactic clasohm@0: val rewtac: thm -> tactic nipkow@1209: val rotate_tac: int -> int -> tactic clasohm@0: val rtac: thm -> int -> tactic clasohm@0: val rule_by_tactic: tactic -> thm -> thm lcp@439: val subgoal_tac: string -> int -> tactic lcp@439: val subgoals_tac: string list -> int -> tactic clasohm@0: val subgoals_of_brl: bool * thm -> int nipkow@1975: val term_lift_inst_rule: nipkow@1975: thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm nipkow@1975: -> thm paulson@1955: val thin_tac: string -> int -> tactic clasohm@0: val trace_goalno_tac: (int -> tactic) -> int -> tactic paulson@1501: end; clasohm@0: clasohm@0: paulson@1501: structure Tactic : TACTIC = clasohm@0: struct clasohm@0: paulson@1501: (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) paulson@1501: fun trace_goalno_tac tac i st = paulson@1501: case Sequence.pull(tac i st) of clasohm@1460: None => Sequence.null clasohm@0: | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); paulson@1501: Sequence.seqof(fn()=> seqcell)); clasohm@0: clasohm@0: paulson@2029: (*Convert all Vars in a theorem to Frees. Also return a function for paulson@2029: reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) paulson@2029: local paulson@2029: fun string_of (a,0) = a paulson@2029: | string_of (a,i) = a ^ "_" ^ string_of_int i; paulson@2029: in paulson@2029: fun freeze_thaw th = paulson@2029: let val fth = freezeT th paulson@2029: val {prop,sign,...} = rep_thm fth paulson@2029: fun mk_inst (Var(v,T)) = paulson@2029: (cterm_of sign (Var(v,T)), paulson@2029: cterm_of sign (Free(string_of v, T))) paulson@2029: val insts = map mk_inst (term_vars prop) paulson@2029: fun thaw th' = paulson@2029: th' |> forall_intr_list (map #2 insts) paulson@2029: |> forall_elim_list (map #1 insts) paulson@2029: in (instantiate ([],insts) fth, thaw) end; paulson@2029: end; paulson@2029: paulson@2029: paulson@2029: (*Rotates the given subgoal to be the last. Useful when re-playing paulson@2029: an old proof script, when the proof of an early subgoal fails. paulson@2029: DOES NOT WORK FOR TYPE VARIABLES.*) paulson@2029: fun defer_tac i state = paulson@2029: let val (state',thaw) = freeze_thaw state paulson@2029: val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) paulson@2029: val hyp::hyps' = drop(i-1,hyps) paulson@2029: in implies_intr hyp (implies_elim_list state' (map assume hyps)) paulson@2029: |> implies_intr_list (take(i-1,hyps) @ hyps') paulson@2029: |> thaw paulson@2029: |> Sequence.single paulson@2029: end paulson@2029: handle _ => Sequence.null; paulson@2029: clasohm@0: clasohm@0: (*Makes a rule by applying a tactic to an existing rule*) paulson@1501: fun rule_by_tactic tac rl = paulson@2029: case rl |> standard |> freeze_thaw |> #1 |> tac |> Sequence.pull of clasohm@1460: None => raise THM("rule_by_tactic", 0, [rl]) clasohm@0: | Some(rl',_) => standard rl'; clasohm@0: clasohm@0: (*** Basic tactics ***) clasohm@0: clasohm@0: (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) paulson@1501: fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null; clasohm@0: clasohm@0: (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) clasohm@0: fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun); clasohm@0: clasohm@0: (*** The following fail if the goal number is out of range: clasohm@0: thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) clasohm@0: clasohm@0: (*Solve subgoal i by assumption*) clasohm@0: fun assume_tac i = PRIMSEQ (assumption i); clasohm@0: clasohm@0: (*Solve subgoal i by assumption, using no unification*) clasohm@0: fun eq_assume_tac i = PRIMITIVE (eq_assumption i); clasohm@0: clasohm@0: (** Resolution/matching tactics **) clasohm@0: clasohm@0: (*The composition rule/state: no lifting or var renaming. clasohm@0: The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) clasohm@0: fun compose_tac arg i = PRIMSEQ (bicompose false arg i); clasohm@0: clasohm@0: (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule clasohm@0: like [| P&Q; P==>R |] ==> R *) clasohm@0: fun make_elim rl = zero_var_indexes (rl RS revcut_rl); clasohm@0: clasohm@0: (*Attack subgoal i by resolution, using flags to indicate elimination rules*) clasohm@0: fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); clasohm@0: clasohm@0: (*Resolution: the simple case, works for introduction rules*) clasohm@0: fun resolve_tac rules = biresolve_tac (map (pair false) rules); clasohm@0: clasohm@0: (*Resolution with elimination rules only*) clasohm@0: fun eresolve_tac rules = biresolve_tac (map (pair true) rules); clasohm@0: clasohm@0: (*Forward reasoning using destruction rules.*) clasohm@0: fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; clasohm@0: clasohm@0: (*Like forward_tac, but deletes the assumption after use.*) clasohm@0: fun dresolve_tac rls = eresolve_tac (map make_elim rls); clasohm@0: clasohm@0: (*Shorthand versions: for resolution with a single theorem*) clasohm@1460: fun rtac rl = resolve_tac [rl]; clasohm@1460: fun etac rl = eresolve_tac [rl]; clasohm@1460: fun dtac rl = dresolve_tac [rl]; clasohm@0: val atac = assume_tac; clasohm@0: clasohm@0: (*Use an assumption or some rules ... A popular combination!*) clasohm@0: fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; clasohm@0: clasohm@0: (*Matching tactics -- as above, but forbid updating of state*) clasohm@0: fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); clasohm@0: fun match_tac rules = bimatch_tac (map (pair false) rules); clasohm@0: fun ematch_tac rules = bimatch_tac (map (pair true) rules); clasohm@0: fun dmatch_tac rls = ematch_tac (map make_elim rls); clasohm@0: clasohm@0: (*Smash all flex-flex disagreement pairs in the proof state.*) clasohm@0: val flexflex_tac = PRIMSEQ flexflex_rule; clasohm@0: clasohm@0: (*Lift and instantiate a rule wrt the given state and subgoal number *) paulson@1501: fun lift_inst_rule (st, i, sinsts, rule) = paulson@1501: let val {maxidx,sign,...} = rep_thm st paulson@1501: val (_, _, Bi, _) = dest_state(st,i) clasohm@1460: val params = Logic.strip_params Bi (*params of subgoal i*) clasohm@0: val params = rev(rename_wrt_term Bi params) (*as they are printed*) clasohm@0: val paramTs = map #2 params clasohm@0: and inc = maxidx+1 clasohm@0: fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) clasohm@0: | liftvar t = raise TERM("Variable expected", [t]); clasohm@0: fun liftterm t = list_abs_free (params, clasohm@1460: Logic.incr_indexes(paramTs,inc) t) clasohm@0: (*Lifts instantiation pair over params*) lcp@230: fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) clasohm@0: fun lifttvar((a,i),ctyp) = clasohm@1460: let val {T,sign} = rep_ctyp ctyp clasohm@1460: in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end paulson@1501: val rts = types_sorts rule and (types,sorts) = types_sorts st clasohm@0: fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) clasohm@0: | types'(ixn) = types ixn; nipkow@949: val used = add_term_tvarnames paulson@1501: (#prop(rep_thm st) $ #prop(rep_thm rule),[]) nipkow@949: val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts clasohm@0: in instantiate (map lifttvar Tinsts, map liftpair insts) paulson@1501: (lift_rule (st,i) rule) clasohm@0: end; clasohm@0: nipkow@1966: (*Like lift_inst_rule but takes cterms, not strings. nipkow@1966: The cterms must be functions of the parameters of the subgoal, nipkow@1966: i.e. they are assumed to be lifted already! nipkow@1966: Also: types of Vars must be fully instantiated already *) nipkow@1975: fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = nipkow@1966: let val {maxidx,sign,...} = rep_thm st nipkow@1966: val (_, _, Bi, _) = dest_state(st,i) nipkow@1966: val params = Logic.strip_params Bi (*params of subgoal i*) nipkow@1966: val paramTs = map #2 params nipkow@1966: and inc = maxidx+1 nipkow@1975: fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T) nipkow@1975: (*lift only Var, not term, which must be lifted already*) nipkow@1975: fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) nipkow@1975: fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) nipkow@1975: in instantiate (map liftTpair Tinsts, map liftpair insts) nipkow@1966: (lift_rule (st,i) rule) nipkow@1966: end; clasohm@0: clasohm@0: (*** Resolve after lifting and instantation; may refer to parameters of the clasohm@0: subgoal. Fails if "i" is out of range. ***) clasohm@0: clasohm@0: (*compose version: arguments are as for bicompose.*) clasohm@0: fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i = paulson@1501: STATE ( fn st => paulson@1501: compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), clasohm@1460: nsubgoal) i clasohm@1460: handle TERM (msg,_) => (writeln msg; no_tac) clasohm@1460: | THM (msg,_,_) => (writeln msg; no_tac) ); clasohm@0: lcp@761: (*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the lcp@761: terms that are substituted contain (term or type) unknowns from the lcp@761: goal, because it is unable to instantiate goal unknowns at the same time. lcp@761: paulson@2029: The type checker is instructed not to freeze flexible type vars that nipkow@952: were introduced during type inference and still remain in the term at the nipkow@952: end. This increases flexibility but can introduce schematic type vars in nipkow@952: goals. lcp@761: *) clasohm@0: fun res_inst_tac sinsts rule i = clasohm@0: compose_inst_tac sinsts (false, rule, nprems_of rule) i; clasohm@0: paulson@1501: (*eresolve elimination version*) clasohm@0: fun eres_inst_tac sinsts rule i = clasohm@0: compose_inst_tac sinsts (true, rule, nprems_of rule) i; clasohm@0: lcp@270: (*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; lcp@270: increment revcut_rl instead.*) clasohm@0: fun make_elim_preserve rl = lcp@270: let val {maxidx,...} = rep_thm rl clasohm@922: fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT)); lcp@270: val revcut_rl' = clasohm@1460: instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), clasohm@1460: (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl clasohm@0: val arg = (false, rl, nprems_of rl) clasohm@0: val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') clasohm@0: in th end clasohm@0: handle Bind => raise THM("make_elim_preserve", 1, [rl]); clasohm@0: lcp@270: (*instantiate and cut -- for a FACT, anyway...*) lcp@270: fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); clasohm@0: lcp@270: (*forward tactic applies a RULE to an assumption without deleting it*) lcp@270: fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; lcp@270: lcp@270: (*dresolve tactic applies a RULE to replace an assumption*) clasohm@0: fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); clasohm@0: paulson@1951: (*Deletion of an assumption*) paulson@1951: fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; paulson@1951: lcp@270: (*** Applications of cut_rl ***) clasohm@0: clasohm@0: (*Used by metacut_tac*) clasohm@0: fun bires_cut_tac arg i = clasohm@1460: resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; clasohm@0: clasohm@0: (*The conclusion of the rule gets assumed in subgoal i, clasohm@0: while subgoal i+1,... are the premises of the rule.*) clasohm@0: fun metacut_tac rule = bires_cut_tac [(false,rule)]; clasohm@0: clasohm@0: (*Recognizes theorems that are not rules, but simple propositions*) clasohm@0: fun is_fact rl = clasohm@0: case prems_of rl of clasohm@1460: [] => true | _::_ => false; clasohm@0: clasohm@0: (*"Cut" all facts from theorem list into the goal as assumptions. *) clasohm@0: fun cut_facts_tac ths i = clasohm@0: EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); clasohm@0: clasohm@0: (*Introduce the given proposition as a lemma and subgoal*) clasohm@0: fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl; clasohm@0: lcp@439: (*Introduce a list of lemmas and subgoals*) lcp@439: fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); lcp@439: clasohm@0: clasohm@0: (**** Indexing and filtering of theorems ****) clasohm@0: clasohm@0: (*Returns the list of potentially resolvable theorems for the goal "prem", clasohm@1460: using the predicate could(subgoal,concl). clasohm@0: Resulting list is no longer than "limit"*) clasohm@0: fun filter_thms could (limit, prem, ths) = clasohm@0: let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) clasohm@0: fun filtr (limit, []) = [] clasohm@1460: | filtr (limit, th::ths) = clasohm@1460: if limit=0 then [] clasohm@1460: else if could(pb, concl_of th) then th :: filtr(limit-1, ths) clasohm@1460: else filtr(limit,ths) clasohm@0: in filtr(limit,ths) end; clasohm@0: clasohm@0: clasohm@0: (*** biresolution and resolution using nets ***) clasohm@0: clasohm@0: (** To preserve the order of the rules, tag them with increasing integers **) clasohm@0: clasohm@0: (*insert tags*) clasohm@0: fun taglist k [] = [] clasohm@0: | taglist k (x::xs) = (k,x) :: taglist (k+1) xs; clasohm@0: clasohm@0: (*remove tags and suppress duplicates -- list is assumed sorted!*) clasohm@0: fun untaglist [] = [] clasohm@0: | untaglist [(k:int,x)] = [x] clasohm@0: | untaglist ((k,x) :: (rest as (k',x')::_)) = clasohm@0: if k=k' then untaglist rest clasohm@0: else x :: untaglist rest; clasohm@0: clasohm@0: (*return list elements in original order*) clasohm@0: val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); clasohm@0: clasohm@0: (*insert one tagged brl into the pair of nets*) lcp@1077: fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = clasohm@0: if eres then clasohm@1460: case prems_of th of clasohm@1460: prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) clasohm@1460: | [] => error"insert_tagged_brl: elimination rule with no premises" clasohm@0: else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); clasohm@0: clasohm@0: (*build a pair of nets for biresolution*) lcp@670: fun build_netpair netpair brls = lcp@1077: foldr insert_tagged_brl (taglist 1 brls, netpair); clasohm@0: paulson@1801: (*delete one kbrl from the pair of nets; paulson@1801: we don't know the value of k, so we use 0 and ignore it in the comparison*) paulson@1801: local paulson@1801: fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th') paulson@1801: in paulson@1801: fun delete_tagged_brl (brl as (eres,th), (inet,enet)) = paulson@1801: if eres then paulson@1801: case prems_of th of paulson@1801: prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl)) paulson@1801: | [] => error"delete_brl: elimination rule with no premises" paulson@1801: else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet); paulson@1801: end; paulson@1801: paulson@1801: clasohm@0: (*biresolution using a pair of nets rather than rules*) clasohm@0: fun biresolution_from_nets_tac match (inet,enet) = clasohm@0: SUBGOAL clasohm@0: (fn (prem,i) => clasohm@0: let val hyps = Logic.strip_assums_hyp prem clasohm@0: and concl = Logic.strip_assums_concl prem clasohm@0: val kbrls = Net.unify_term inet concl @ clasohm@0: flat (map (Net.unify_term enet) hyps) clasohm@0: in PRIMSEQ (biresolution match (orderlist kbrls) i) end); clasohm@0: clasohm@0: (*versions taking pre-built nets*) clasohm@0: val biresolve_from_nets_tac = biresolution_from_nets_tac false; clasohm@0: val bimatch_from_nets_tac = biresolution_from_nets_tac true; clasohm@0: clasohm@0: (*fast versions using nets internally*) lcp@670: val net_biresolve_tac = lcp@670: biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); lcp@670: lcp@670: val net_bimatch_tac = lcp@670: bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); clasohm@0: clasohm@0: (*** Simpler version for resolve_tac -- only one net, and no hyps ***) clasohm@0: clasohm@0: (*insert one tagged rl into the net*) clasohm@0: fun insert_krl (krl as (k,th), net) = clasohm@0: Net.insert_term ((concl_of th, krl), net, K false); clasohm@0: clasohm@0: (*build a net of rules for resolution*) clasohm@0: fun build_net rls = clasohm@0: foldr insert_krl (taglist 1 rls, Net.empty); clasohm@0: clasohm@0: (*resolution using a net rather than rules; pred supports filt_resolve_tac*) clasohm@0: fun filt_resolution_from_net_tac match pred net = clasohm@0: SUBGOAL clasohm@0: (fn (prem,i) => clasohm@0: let val krls = Net.unify_term net (Logic.strip_assums_concl prem) clasohm@0: in clasohm@1460: if pred krls clasohm@0: then PRIMSEQ clasohm@1460: (biresolution match (map (pair false) (orderlist krls)) i) clasohm@0: else no_tac clasohm@0: end); clasohm@0: clasohm@0: (*Resolve the subgoal using the rules (making a net) unless too flexible, clasohm@0: which means more than maxr rules are unifiable. *) clasohm@0: fun filt_resolve_tac rules maxr = clasohm@0: let fun pred krls = length krls <= maxr clasohm@0: in filt_resolution_from_net_tac false pred (build_net rules) end; clasohm@0: clasohm@0: (*versions taking pre-built nets*) clasohm@0: val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); clasohm@0: val match_from_net_tac = filt_resolution_from_net_tac true (K true); clasohm@0: clasohm@0: (*fast versions using nets internally*) clasohm@0: val net_resolve_tac = resolve_from_net_tac o build_net; clasohm@0: val net_match_tac = match_from_net_tac o build_net; clasohm@0: clasohm@0: clasohm@0: (*** For Natural Deduction using (bires_flg, rule) pairs ***) clasohm@0: clasohm@0: (*The number of new subgoals produced by the brule*) lcp@1077: fun subgoals_of_brl (true,rule) = nprems_of rule - 1 lcp@1077: | subgoals_of_brl (false,rule) = nprems_of rule; clasohm@0: clasohm@0: (*Less-than test: for sorting to minimize number of new subgoals*) clasohm@0: fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; clasohm@0: clasohm@0: clasohm@0: (*** Meta-Rewriting Tactics ***) clasohm@0: clasohm@0: fun result1 tacf mss thm = paulson@1501: case Sequence.pull(tacf mss thm) of clasohm@0: None => None clasohm@0: | Some(thm,_) => Some(thm); clasohm@0: clasohm@0: (*Rewrite subgoal i only *) nipkow@214: fun asm_rewrite_goal_tac mode prover_tac mss i = nipkow@214: PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i); clasohm@0: lcp@69: (*Rewrite throughout proof state. *) lcp@69: fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); clasohm@0: clasohm@0: (*Rewrite subgoals only, not main goal. *) lcp@69: fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); clasohm@0: clasohm@1460: fun rewtac def = rewrite_goals_tac [def]; clasohm@0: clasohm@0: paulson@1501: (*** for folding definitions, handling critical pairs ***) lcp@69: lcp@69: (*The depth of nesting in a term*) lcp@69: fun term_depth (Abs(a,T,t)) = 1 + term_depth t lcp@69: | term_depth (f$t) = 1 + max [term_depth f, term_depth t] lcp@69: | term_depth _ = 0; lcp@69: lcp@69: val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm; lcp@69: lcp@69: (*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) lcp@69: Returns longest lhs first to avoid folding its subexpressions.*) lcp@69: fun sort_lhs_depths defs = lcp@69: let val keylist = make_keylist (term_depth o lhs_of_thm) defs lcp@69: val keys = distinct (sort op> (map #2 keylist)) lcp@69: in map (keyfilter keylist) keys end; lcp@69: lcp@69: fun fold_tac defs = EVERY lcp@69: (map rewrite_tac (sort_lhs_depths (map symmetric defs))); lcp@69: lcp@69: fun fold_goals_tac defs = EVERY lcp@69: (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); lcp@69: lcp@69: lcp@69: (*** Renaming of parameters in a subgoal lcp@69: Names may contain letters, digits or primes and must be lcp@69: separated by blanks ***) clasohm@0: clasohm@0: (*Calling this will generate the warning "Same as previous level" since clasohm@0: it affects nothing but the names of bound variables!*) clasohm@0: fun rename_tac str i = clasohm@0: let val cs = explode str clasohm@0: in clasohm@0: if !Logic.auto_rename clasohm@0: then (writeln"Note: setting Logic.auto_rename := false"; clasohm@1460: Logic.auto_rename := false) clasohm@0: else (); clasohm@0: case #2 (take_prefix (is_letdig orf is_blank) cs) of clasohm@0: [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i)) clasohm@0: | c::_ => error ("Illegal character: " ^ c) clasohm@0: end; clasohm@0: paulson@1501: (*Rename recent parameters using names generated from a and the suffixes, paulson@1501: provided the string a, which represents a term, is an identifier. *) clasohm@0: fun rename_last_tac a sufs i = clasohm@0: let val names = map (curry op^ a) sufs clasohm@0: in if Syntax.is_identifier a clasohm@0: then PRIMITIVE (rename_params_rule (names,i)) clasohm@0: else all_tac clasohm@0: end; clasohm@0: clasohm@0: (*Prunes all redundant parameters from the proof state by rewriting*) clasohm@0: val prune_params_tac = rewrite_tac [triv_forall_equality]; clasohm@0: paulson@1501: (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from paulson@1501: right to left if n is positive, and from left to right if n is negative.*) nipkow@1209: fun rotate_tac n = nipkow@1209: let fun rot(n) = EVERY'(replicate n (dtac asm_rl)); nipkow@1209: in if n >= 0 then rot n nipkow@1209: else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i) nipkow@1209: end; nipkow@1209: clasohm@0: end; paulson@1501: paulson@1501: open Tactic;