wenzelm@10805: (* Title: Pure/tactic.ML wenzelm@10805: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: wenzelm@29276: Fundamental tactics. clasohm@0: *) clasohm@0: wenzelm@11774: signature BASIC_TACTIC = wenzelm@11774: sig wenzelm@23223: val trace_goalno_tac: (int -> tactic) -> int -> tactic wenzelm@23223: val rule_by_tactic: tactic -> thm -> thm wenzelm@23223: val assume_tac: int -> tactic wenzelm@23223: val eq_assume_tac: int -> tactic wenzelm@23223: val compose_tac: (bool * thm * int) -> int -> tactic wenzelm@23223: val make_elim: thm -> thm wenzelm@23223: val biresolve_tac: (bool * thm) list -> int -> tactic wenzelm@23223: val resolve_tac: thm list -> int -> tactic wenzelm@23223: val eresolve_tac: thm list -> int -> tactic wenzelm@23223: val forward_tac: thm list -> int -> tactic wenzelm@23223: val dresolve_tac: thm list -> int -> tactic wenzelm@23223: val atac: int -> tactic wenzelm@23223: val rtac: thm -> int -> tactic haftmann@31251: val dtac: thm -> int -> tactic haftmann@31251: val etac: thm -> int -> tactic haftmann@31251: val ftac: thm -> int -> tactic wenzelm@23223: val datac: thm -> int -> int -> tactic wenzelm@23223: val eatac: thm -> int -> int -> tactic wenzelm@23223: val fatac: thm -> int -> int -> tactic wenzelm@23223: val ares_tac: thm list -> int -> tactic wenzelm@23223: val solve_tac: thm list -> int -> tactic wenzelm@23223: val bimatch_tac: (bool * thm) list -> int -> tactic wenzelm@23223: val match_tac: thm list -> int -> tactic wenzelm@23223: val ematch_tac: thm list -> int -> tactic wenzelm@23223: val dmatch_tac: thm list -> int -> tactic wenzelm@23223: val flexflex_tac: tactic wenzelm@23223: val distinct_subgoal_tac: int -> tactic wenzelm@23223: val distinct_subgoals_tac: tactic wenzelm@23223: val metacut_tac: thm -> int -> tactic wenzelm@23223: val cut_rules_tac: thm list -> int -> tactic wenzelm@23223: val cut_facts_tac: thm list -> int -> tactic wenzelm@23223: val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list wenzelm@23223: val biresolution_from_nets_tac: ('a list -> (bool * thm) list) -> wenzelm@23223: bool -> 'a Net.net * 'a Net.net -> int -> tactic wenzelm@23223: val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> wenzelm@23223: int -> tactic wenzelm@23223: val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> wenzelm@23223: int -> tactic wenzelm@23223: val net_biresolve_tac: (bool * thm) list -> int -> tactic wenzelm@23223: val net_bimatch_tac: (bool * thm) list -> int -> tactic wenzelm@23223: val filt_resolve_tac: thm list -> int -> int -> tactic wenzelm@23223: val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic wenzelm@23223: val match_from_net_tac: (int * thm) Net.net -> int -> tactic wenzelm@23223: val net_resolve_tac: thm list -> int -> tactic wenzelm@23223: val net_match_tac: thm list -> int -> tactic wenzelm@23223: val subgoals_of_brl: bool * thm -> int wenzelm@23223: val lessb: (bool * thm) * (bool * thm) -> bool wenzelm@27243: val rename_tac: string list -> int -> tactic wenzelm@23223: val rotate_tac: int -> int -> tactic wenzelm@23223: val defer_tac: int -> tactic wenzelm@23223: val filter_prems_tac: (term -> bool) -> int -> tactic wenzelm@11774: end; clasohm@0: wenzelm@11774: signature TACTIC = wenzelm@11774: sig wenzelm@11774: include BASIC_TACTIC wenzelm@11929: val innermost_params: int -> thm -> (string * typ) list wenzelm@27243: val term_lift_inst_rule: wenzelm@27243: thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm wenzelm@23223: val insert_tagged_brl: 'a * (bool * thm) -> wenzelm@23223: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> wenzelm@23223: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net wenzelm@23223: val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> wenzelm@23223: (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net wenzelm@23223: val delete_tagged_brl: bool * thm -> wenzelm@23223: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> wenzelm@23223: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net wenzelm@23223: val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool wenzelm@32971: val build_net: thm list -> (int * thm) Net.net wenzelm@11774: end; clasohm@0: wenzelm@11774: structure Tactic: TACTIC = clasohm@0: struct clasohm@0: paulson@1501: (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) wenzelm@10817: fun trace_goalno_tac tac i st = wenzelm@4270: case Seq.pull(tac i st) of skalberg@15531: NONE => Seq.empty wenzelm@12262: | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); wenzelm@10805: Seq.make(fn()=> seqcell)); clasohm@0: clasohm@0: (*Makes a rule by applying a tactic to an existing rule*) paulson@1501: fun rule_by_tactic tac rl = wenzelm@19925: let wenzelm@19925: val ctxt = Variable.thm_context rl; wenzelm@31794: val ((_, [st]), ctxt') = Variable.import true [rl] ctxt; wenzelm@19925: in wenzelm@19925: (case Seq.pull (tac st) of wenzelm@19925: NONE => raise THM ("rule_by_tactic", 0, [rl]) wenzelm@19925: | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) paulson@2688: end; wenzelm@10817: wenzelm@19925: clasohm@0: (*** Basic tactics ***) 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*) wenzelm@31945: fun assume_tac i = PRIMSEQ (Thm.assumption i); clasohm@0: clasohm@0: (*Solve subgoal i by assumption, using no unification*) wenzelm@31945: fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i); clasohm@0: wenzelm@23223: clasohm@0: (** Resolution/matching tactics **) clasohm@0: clasohm@0: (*The composition rule/state: no lifting or var renaming. wenzelm@31945: The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*) wenzelm@31945: fun compose_tac arg i = PRIMSEQ (Thm.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*) wenzelm@31945: fun biresolve_tac brules i = PRIMSEQ (Thm.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*) oheimb@7491: val atac = assume_tac; oheimb@7491: fun rtac rl = resolve_tac [rl]; oheimb@7491: fun dtac rl = dresolve_tac [rl]; clasohm@1460: fun etac rl = eresolve_tac [rl]; oheimb@7491: fun ftac rl = forward_tac [rl]; oheimb@7491: fun datac thm j = EVERY' (dtac thm::replicate j atac); oheimb@7491: fun eatac thm j = EVERY' (etac thm::replicate j atac); oheimb@7491: fun fatac thm j = EVERY' (ftac thm::replicate j atac); 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: wenzelm@5263: fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; wenzelm@5263: clasohm@0: (*Matching tactics -- as above, but forbid updating of state*) wenzelm@31945: fun bimatch_tac brules i = PRIMSEQ (Thm.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: wenzelm@19056: (*Remove duplicate subgoals.*) paulson@22560: val perm_tac = PRIMITIVE oo Thm.permute_prems; paulson@22560: paulson@22560: fun distinct_tac (i, k) = paulson@22560: perm_tac 0 (i - 1) THEN paulson@22560: perm_tac 1 (k - 1) THEN paulson@22560: DETERM (PRIMSEQ (fn st => paulson@22560: Thm.compose_no_flatten false (st, 0) 1 paulson@22560: (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN paulson@22560: perm_tac 1 (1 - k) THEN paulson@22560: perm_tac 0 (1 - i); paulson@22560: paulson@22560: fun distinct_subgoal_tac i st = haftmann@33955: (case (uncurry drop) (i - 1, Thm.prems_of st) of paulson@22560: [] => no_tac st paulson@22560: | A :: Bs => paulson@22560: st |> EVERY (fold (fn (B, k) => wenzelm@23223: if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) [])); paulson@22560: wenzelm@10817: fun distinct_subgoals_tac state = wenzelm@19056: let wenzelm@19056: val goals = Thm.prems_of state; wenzelm@19056: val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals)); wenzelm@19056: in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end; paulson@3409: wenzelm@11929: (*Determine print names of goal parameters (reversed)*) wenzelm@11929: fun innermost_params i st = wenzelm@11929: let val (_, _, Bi, _) = dest_state (st, i) wenzelm@29276: in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; wenzelm@11929: paulson@15453: (*params of subgoal i as they are printed*) paulson@19532: fun params_of_state i st = rev (innermost_params i st); wenzelm@16425: nipkow@3984: (* nipkow@3984: Like lift_inst_rule but takes terms, not strings, where the terms may contain nipkow@3984: Bounds referring to parameters of the subgoal. nipkow@3984: nipkow@3984: insts: [...,(vj,tj),...] nipkow@3984: nipkow@3984: The tj may contain references to parameters of subgoal i of the state st nipkow@3984: in the form of Bound k, i.e. the tj may be subterms of the subgoal. nipkow@3984: To saturate the lose bound vars, the tj are enclosed in abstractions nipkow@3984: corresponding to the parameters of subgoal i, thus turning them into nipkow@3984: functions. At the same time, the types of the vj are lifted. nipkow@3984: nipkow@3984: NB: the types in insts must be correctly instantiated already, nipkow@3984: i.e. Tinsts is not applied to insts. nipkow@3984: *) nipkow@1975: fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = wenzelm@26626: let wenzelm@26626: val thy = Thm.theory_of_thm st wenzelm@26626: val cert = Thm.cterm_of thy wenzelm@26626: val certT = Thm.ctyp_of thy wenzelm@26626: val maxidx = Thm.maxidx_of st paulson@19532: val paramTs = map #2 (params_of_state i st) wenzelm@26626: val inc = maxidx+1 wenzelm@16876: fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T) nipkow@1975: (*lift only Var, not term, which must be lifted already*) wenzelm@26626: fun liftpair (v,t) = (cert (liftvar v), cert t) berghofe@15797: fun liftTpair (((a, i), S), T) = wenzelm@26626: (certT (TVar ((a, i + inc), S)), wenzelm@26626: certT (Logic.incr_tvar inc T)) paulson@8129: in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) wenzelm@18145: (Thm.lift_rule (Thm.cprem_of st i) rule) nipkow@1966: end; clasohm@0: clasohm@0: paulson@1951: lcp@270: (*** Applications of cut_rl ***) 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.*) wenzelm@27243: fun metacut_tac rule i = resolve_tac [cut_rl] i THEN biresolve_tac [(false, rule)] (i+1); clasohm@0: paulson@13650: (*"Cut" a list of rules into the goal. Their premises will become new paulson@13650: subgoals.*) paulson@13650: fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths); paulson@13650: paulson@13650: (*As above, but inserts only facts (unconditional theorems); paulson@13650: generates no additional subgoals. *) wenzelm@20232: fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths); clasohm@0: clasohm@0: clasohm@0: (**** Indexing and filtering of theorems ****) clasohm@0: clasohm@0: (*Returns the list of potentially resolvable theorems for the goal "prem", wenzelm@10805: 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, []) = [] wenzelm@10805: | filtr (limit, th::ths) = wenzelm@10805: if limit=0 then [] wenzelm@10805: else if could(pb, concl_of th) then th :: filtr(limit-1, ths) wenzelm@10805: 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 one tagged brl into the pair of nets*) wenzelm@23178: fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) = wenzelm@12320: if eres then wenzelm@12320: (case try Thm.major_prem_of th of wenzelm@16809: SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet) skalberg@15531: | NONE => error "insert_tagged_brl: elimination rule with no premises") wenzelm@16809: else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet); clasohm@0: clasohm@0: (*build a pair of nets for biresolution*) wenzelm@10817: fun build_netpair netpair brls = wenzelm@30558: fold_rev insert_tagged_brl (tag_list 1 brls) netpair; clasohm@0: wenzelm@12320: (*delete one kbrl from the pair of nets*) wenzelm@22360: fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') wenzelm@16809: wenzelm@23178: fun delete_tagged_brl (brl as (eres, th)) (inet, enet) = paulson@13925: (if eres then wenzelm@12320: (case try Thm.major_prem_of th of wenzelm@16809: SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet) skalberg@15531: | NONE => (inet, enet)) (*no major premise: ignore*) wenzelm@16809: else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet)) paulson@13925: handle Net.DELETE => (inet,enet); paulson@1801: paulson@1801: wenzelm@10817: (*biresolution using a pair of nets rather than rules. paulson@3706: function "order" must sort and possibly filter the list of brls. paulson@3706: boolean "match" indicates matching or unification.*) paulson@3706: fun biresolution_from_nets_tac order match (inet,enet) = clasohm@0: SUBGOAL clasohm@0: (fn (prem,i) => clasohm@0: let val hyps = Logic.strip_assums_hyp prem wenzelm@10817: and concl = Logic.strip_assums_concl prem wenzelm@19482: val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps wenzelm@31945: in PRIMSEQ (Thm.biresolution match (order kbrls) i) end); clasohm@0: paulson@3706: (*versions taking pre-built nets. No filtering of brls*) wenzelm@30558: val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false; wenzelm@30558: val bimatch_from_nets_tac = biresolution_from_nets_tac order_list 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*) wenzelm@23178: fun insert_krl (krl as (k,th)) = wenzelm@23178: Net.insert_term (K false) (concl_of th, krl); clasohm@0: clasohm@0: (*build a net of rules for resolution*) wenzelm@10817: fun build_net rls = wenzelm@30558: fold_rev insert_krl (tag_list 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) wenzelm@10817: in wenzelm@10817: if pred krls clasohm@0: then PRIMSEQ wenzelm@31945: (Thm.biresolution match (map (pair false) (order_list 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. *) wenzelm@10817: 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: wenzelm@27243: (*Renaming of parameters in a subgoal*) wenzelm@27243: fun rename_tac xs i = wenzelm@14673: case Library.find_first (not o Syntax.is_identifier) xs of skalberg@15531: SOME x => error ("Not an identifier: " ^ x) wenzelm@31945: | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i)); wenzelm@9535: 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.*) paulson@2672: fun rotate_tac 0 i = all_tac wenzelm@31945: | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i); nipkow@1209: paulson@7248: (*Rotates the given subgoal to be the last.*) wenzelm@31945: fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1); paulson@7248: nipkow@5974: (* remove premises that do not satisfy p; fails if all prems satisfy p *) nipkow@5974: fun filter_prems_tac p = skalberg@15531: let fun Then NONE tac = SOME tac skalberg@15531: | Then (SOME tac) tac' = SOME(tac THEN' tac'); wenzelm@19473: fun thins H (tac,n) = nipkow@5974: if p H then (tac,n+1) nipkow@5974: else (Then tac (rotate_tac n THEN' etac thin_rl),0); nipkow@5974: in SUBGOAL(fn (subg,n) => nipkow@5974: let val Hs = Logic.strip_assums_hyp subg wenzelm@19473: in case fst(fold thins Hs (NONE,0)) of skalberg@15531: NONE => no_tac | SOME tac => tac n nipkow@5974: end) nipkow@5974: end; nipkow@5974: clasohm@0: end; paulson@1501: wenzelm@32971: structure Basic_Tactic: BASIC_TACTIC = Tactic; wenzelm@32971: open Basic_Tactic;