wenzelm@10805: (* Title: Pure/tactic.ML clasohm@0: ID: $Id$ wenzelm@10805: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1991 University of Cambridge clasohm@0: wenzelm@10805: Tactics. clasohm@0: *) clasohm@0: wenzelm@11774: signature BASIC_TACTIC = wenzelm@11774: sig wenzelm@10805: val ares_tac : thm list -> int -> tactic wenzelm@10805: val assume_tac : int -> tactic wenzelm@10805: val atac : int ->tactic wenzelm@10817: val bimatch_from_nets_tac: paulson@1501: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic wenzelm@10805: val bimatch_tac : (bool*thm)list -> int -> tactic wenzelm@10817: val biresolution_from_nets_tac: wenzelm@10805: ('a list -> (bool * thm) list) -> wenzelm@10805: bool -> 'a Net.net * 'a Net.net -> int -> tactic wenzelm@10817: val biresolve_from_nets_tac: paulson@1501: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic wenzelm@10805: val biresolve_tac : (bool*thm)list -> int -> tactic wenzelm@10805: 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 wenzelm@10817: val compose_inst_tac : (string*string)list -> (bool*thm*int) -> paulson@3409: int -> tactic wenzelm@10817: val compose_tac : (bool * thm * int) -> int -> tactic wenzelm@10805: val cut_facts_tac : thm list -> int -> tactic paulson@13650: val cut_rules_tac : thm list -> int -> tactic wenzelm@10817: val cut_inst_tac : (string*string)list -> thm -> int -> tactic oheimb@7491: val datac : thm -> int -> int -> tactic wenzelm@10805: val defer_tac : int -> tactic wenzelm@10805: val distinct_subgoals_tac : tactic wenzelm@10805: val dmatch_tac : thm list -> int -> tactic wenzelm@10805: val dresolve_tac : thm list -> int -> tactic wenzelm@10817: val dres_inst_tac : (string*string)list -> thm -> int -> tactic wenzelm@10805: val dtac : thm -> int ->tactic oheimb@7491: val eatac : thm -> int -> int -> tactic wenzelm@10805: val etac : thm -> int ->tactic wenzelm@10817: val eq_assume_tac : int -> tactic wenzelm@10805: val ematch_tac : thm list -> int -> tactic wenzelm@10805: val eresolve_tac : thm list -> int -> tactic wenzelm@10805: val eres_inst_tac : (string*string)list -> thm -> int -> tactic oheimb@7491: val fatac : thm -> int -> int -> tactic wenzelm@10817: val filter_prems_tac : (term -> bool) -> int -> tactic wenzelm@10805: val filter_thms : (term*term->bool) -> int*term*thm list -> thm list wenzelm@10805: val filt_resolve_tac : thm list -> int -> int -> tactic wenzelm@10805: val flexflex_tac : tactic wenzelm@10805: val fold_goals_tac : thm list -> tactic wenzelm@10805: val fold_rule : thm list -> thm -> thm wenzelm@10805: val fold_tac : thm list -> tactic wenzelm@10817: val forward_tac : thm list -> int -> tactic wenzelm@10805: val forw_inst_tac : (string*string)list -> thm -> int -> tactic wenzelm@10805: val ftac : thm -> int ->tactic wenzelm@12320: val insert_tagged_brl : ('a * (bool * thm)) * wenzelm@12320: (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) -> wenzelm@12320: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net wenzelm@12320: val delete_tagged_brl : (bool * thm) * wenzelm@12320: (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) -> wenzelm@12320: ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net wenzelm@10805: val is_fact : thm -> bool wenzelm@10805: val lessb : (bool * thm) * (bool * thm) -> bool wenzelm@10805: val lift_inst_rule : thm * int * (string*string)list * thm -> thm wenzelm@10805: val make_elim : thm -> thm wenzelm@10805: val match_from_net_tac : (int*thm) Net.net -> int -> tactic wenzelm@10805: val match_tac : thm list -> int -> tactic wenzelm@10805: val metacut_tac : thm -> int -> tactic wenzelm@10805: val net_bimatch_tac : (bool*thm) list -> int -> tactic wenzelm@10805: val net_biresolve_tac : (bool*thm) list -> int -> tactic wenzelm@10805: val net_match_tac : thm list -> int -> tactic wenzelm@10805: val net_resolve_tac : thm list -> int -> tactic ballarin@15696: val norm_hhf_plain : thm -> thm wenzelm@12801: val norm_hhf_rule : thm -> thm wenzelm@10805: val norm_hhf_tac : int -> tactic wenzelm@10805: val prune_params_tac : tactic wenzelm@10805: val rename_params_tac : string list -> int -> tactic wenzelm@10805: val rename_tac : string -> int -> tactic wenzelm@10805: val rename_last_tac : string -> string list -> int -> tactic wenzelm@10805: val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic wenzelm@10805: val resolve_tac : thm list -> int -> tactic wenzelm@10817: val res_inst_tac : (string*string)list -> thm -> int -> tactic wenzelm@10444: val rewrite_goal_tac : thm list -> int -> tactic wenzelm@3575: val rewrite_goals_rule: thm list -> thm -> thm wenzelm@10805: val rewrite_rule : thm list -> thm -> thm wenzelm@10805: val rewrite_goals_tac : thm list -> tactic wenzelm@10805: val rewrite_tac : thm list -> tactic wenzelm@10805: val rewtac : thm -> tactic wenzelm@10805: val rotate_tac : int -> int -> tactic wenzelm@10805: val rtac : thm -> int -> tactic wenzelm@10805: val rule_by_tactic : tactic -> thm -> thm wenzelm@10805: val solve_tac : thm list -> int -> tactic wenzelm@10805: val subgoal_tac : string -> int -> tactic wenzelm@10805: val subgoals_tac : string list -> int -> tactic wenzelm@10805: val subgoals_of_brl : bool * thm -> int wenzelm@10805: val term_lift_inst_rule : berghofe@15797: thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm nipkow@1975: -> thm oheimb@10347: val instantiate_tac : (string * string) list -> tactic wenzelm@10805: val thin_tac : string -> int -> tactic wenzelm@10805: val trace_goalno_tac : (int -> tactic) -> 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@11774: val untaglist: (int * 'a) list -> 'a list wenzelm@16809: val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool wenzelm@11774: val orderlist: (int * 'a) list -> 'a list wenzelm@11774: val rewrite: bool -> thm list -> cterm -> thm wenzelm@11774: val simplify: bool -> thm list -> thm -> thm wenzelm@12139: val conjunction_tac: tactic wenzelm@15874: val smart_conjunction_tac: int -> tactic wenzelm@16425: val prove_multi_plain: theory -> string list -> term list -> term list -> ballarin@16325: (thm list -> tactic) -> thm list wenzelm@16425: val prove_multi: theory -> string list -> term list -> term list -> wenzelm@15874: (thm list -> tactic) -> thm list wenzelm@16425: val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm wenzelm@16425: val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm berghofe@15442: val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) -> berghofe@15442: int -> tactic berghofe@15442: val lift_inst_rule' : thm * int * (indexname * string) list * thm -> thm berghofe@15464: val eres_inst_tac' : (indexname * string) list -> thm -> int -> tactic berghofe@15442: val res_inst_tac' : (indexname * string) list -> thm -> int -> tactic berghofe@15797: val instantiate_tac' : (indexname * string) list -> tactic 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 = paulson@2688: let val (st, thaw) = freeze_thaw (zero_var_indexes rl) wenzelm@4270: in case Seq.pull (tac st) of skalberg@15531: NONE => raise THM("rule_by_tactic", 0, [rl]) skalberg@15531: | SOME(st',_) => Thm.varifyT (thaw st') paulson@2688: end; wenzelm@10817: 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*) 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*) 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*) 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: paulson@3409: paulson@3409: (*Remove duplicate subgoals. By Mark Staples*) paulson@3409: local wenzelm@16666: fun cterm_aconv (a,b) = term_of a aconv term_of b; paulson@3409: in wenzelm@10817: fun distinct_subgoals_tac state = paulson@3409: let val (frozth,thawfn) = freeze_thaw state wenzelm@10805: val froz_prems = cprems_of frozth wenzelm@10805: val assumed = implies_elim_list frozth (map assume froz_prems) wenzelm@10805: val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) wenzelm@10805: assumed; paulson@15977: in (*Applying Thm.varifyT to the result of thawfn would (re-)generalize paulson@15977: all type variables that appear in the subgoals. Unfortunately, it paulson@15977: would also break the function AxClass.intro_classes_tac, even in the paulson@15977: trivial case where the type class has no axioms.*) paulson@15977: Seq.single (thawfn implied) paulson@15977: end wenzelm@10817: end; paulson@3409: 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@11929: in rename_wrt_term Bi (Logic.strip_params Bi) end; wenzelm@11929: paulson@15453: (*params of subgoal i as they are printed*) paulson@15453: fun params_of_state st i = paulson@15453: let val (_, _, Bi, _) = dest_state(st,i) paulson@15453: val params = Logic.strip_params Bi paulson@15453: in rev(rename_wrt_term Bi params) end; wenzelm@16425: paulson@15453: (*read instantiations with respect to subgoal i of proof state st*) paulson@15453: fun read_insts_in_state (st, i, sinsts, rule) = wenzelm@16425: let val thy = Thm.theory_of_thm st wenzelm@16425: and params = params_of_state st i wenzelm@16425: and rts = types_sorts rule and (types,sorts) = types_sorts st haftmann@17271: fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm) wenzelm@16425: | types' ixn = types ixn; wenzelm@16425: val used = Drule.add_used rule (Drule.add_used st []); wenzelm@16425: in read_insts thy rts (types',sorts) used sinsts end; paulson@15453: clasohm@0: (*Lift and instantiate a rule wrt the given state and subgoal number *) berghofe@15442: fun lift_inst_rule' (st, i, sinsts, rule) = paulson@15453: let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) paulson@15453: and {maxidx,...} = rep_thm st paulson@15453: and params = params_of_state st i clasohm@0: val paramTs = map #2 params clasohm@0: and inc = maxidx+1 wenzelm@16876: fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T) clasohm@0: | liftvar t = raise TERM("Variable expected", [t]); wenzelm@10817: fun liftterm t = list_abs_free (params, wenzelm@10805: 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) wenzelm@16876: val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc)) paulson@8129: in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) paulson@8129: (lift_rule (st,i) rule) clasohm@0: end; clasohm@0: berghofe@15442: fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' berghofe@15442: (st, i, map (apfst Syntax.indexname) sinsts, rule); berghofe@15442: 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@16425: let val {maxidx,thy,...} = rep_thm st paulson@15453: val paramTs = map #2 (params_of_state st i) nipkow@1966: and 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@16425: fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) berghofe@15797: fun liftTpair (((a, i), S), T) = wenzelm@16425: (ctyp_of thy (TVar ((a, i + inc), S)), wenzelm@16876: ctyp_of thy (Logic.incr_tvar inc T)) paulson@8129: in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) paulson@8129: (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.*) berghofe@15442: fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st = paulson@8977: if i > nprems_of st then no_tac st paulson@8977: else st |> berghofe@15442: (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i wenzelm@12262: handle TERM (msg,_) => (warning msg; no_tac) wenzelm@12262: | THM (msg,_,_) => (warning msg; no_tac)); clasohm@0: berghofe@15442: val compose_inst_tac = gen_compose_inst_tac lift_inst_rule; berghofe@15442: val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule'; berghofe@15442: 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: berghofe@15442: fun res_inst_tac' sinsts rule i = berghofe@15442: compose_inst_tac' sinsts (false, rule, nprems_of rule) i; berghofe@15442: 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: berghofe@15464: fun eres_inst_tac' sinsts rule i = berghofe@15464: compose_inst_tac' sinsts (true, rule, nprems_of rule) i; berghofe@15464: lcp@270: (*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; lcp@270: increment revcut_rl instead.*) wenzelm@10817: fun make_elim_preserve rl = lcp@270: let val {maxidx,...} = rep_thm rl wenzelm@16425: fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT)); wenzelm@10817: val revcut_rl' = wenzelm@10805: instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), wenzelm@10805: (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl clasohm@0: val arg = (false, rl, nprems_of rl) wenzelm@4270: val [th] = Seq.list_of (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: oheimb@10347: (*instantiate variables in the whole state*) oheimb@10347: val instantiate_tac = PRIMITIVE o read_instantiate; oheimb@10347: berghofe@15797: val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; berghofe@15797: 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 wenzelm@10805: [] => true | _::_ => false; 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. *) skalberg@15570: fun cut_facts_tac ths = cut_rules_tac (List.filter is_fact ths); clasohm@0: clasohm@0: (*Introduce the given proposition as a lemma and subgoal*) wenzelm@12847: fun subgoal_tac sprop = wenzelm@12847: DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) => wenzelm@12847: let val concl' = Logic.strip_assums_concl prop in paulson@4178: if null (term_tvars concl') then () paulson@4178: else warning"Type variables in new subgoal: add a type constraint?"; wenzelm@12847: all_tac wenzelm@12847: end); 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", 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 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*) wenzelm@10817: fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); clasohm@0: clasohm@0: (*insert one tagged brl into the pair of nets*) wenzelm@12320: 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 = skalberg@15574: foldr insert_tagged_brl netpair (taglist 1 brls); clasohm@0: wenzelm@12320: (*delete one kbrl from the pair of nets*) wenzelm@16809: fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') wenzelm@16809: wenzelm@12320: 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 clasohm@0: val kbrls = Net.unify_term inet concl @ paulson@2672: List.concat (map (Net.unify_term enet) hyps) paulson@3706: in PRIMSEQ (biresolution match (order kbrls) i) end); clasohm@0: paulson@3706: (*versions taking pre-built nets. No filtering of brls*) paulson@3706: val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false; paulson@3706: val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist 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) = wenzelm@16809: Net.insert_term (K false) (concl_of th, krl) net; clasohm@0: clasohm@0: (*build a net of rules for resolution*) wenzelm@10817: fun build_net rls = skalberg@15574: foldr insert_krl Net.empty (taglist 1 rls); 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@10805: (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. *) 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: clasohm@0: (*** Meta-Rewriting Tactics ***) clasohm@0: wenzelm@3575: val simple_prover = wenzelm@15021: SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss))); wenzelm@3575: wenzelm@11768: val rewrite = MetaSimplifier.rewrite_aux simple_prover; wenzelm@11768: val simplify = MetaSimplifier.simplify_aux simple_prover; wenzelm@11768: val rewrite_rule = simplify true; berghofe@10415: val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover; wenzelm@3575: wenzelm@10444: fun rewrite_goal_tac rews = wenzelm@15021: MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) wenzelm@15021: (MetaSimplifier.empty_ss addsimps rews); wenzelm@10444: 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@1460: fun rewtac def = rewrite_goals_tac [def]; clasohm@0: ballarin@15696: fun norm_hhf_plain th = wenzelm@16942: if Drule.is_norm_hhf (Thm.prop_of th) then th ballarin@15696: else rewrite_rule [Drule.norm_hhf_eq] th; ballarin@15696: wenzelm@16942: val norm_hhf_rule = wenzelm@16942: norm_hhf_plain wenzelm@16942: #> Thm.adjust_maxidx_thm wenzelm@16942: #> Drule.gen_all; wenzelm@10817: wenzelm@12782: val norm_hhf_tac = wenzelm@12782: rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*) wenzelm@12782: THEN' SUBGOAL (fn (t, i) => wenzelm@12801: if Drule.is_norm_hhf t then all_tac wenzelm@12782: else rewrite_goal_tac [Drule.norm_hhf_eq] i); wenzelm@10805: 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 paulson@2145: | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t) lcp@69: | term_depth _ = 0; lcp@69: wenzelm@12801: val lhs_of_thm = #1 o Logic.dest_equals o prop_of; 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 = haftmann@17496: let val keylist = AList.make (term_depth o lhs_of_thm) defs wenzelm@4438: val keys = distinct (sort (rev_order o int_ord) (map #2 keylist)) haftmann@17496: in map (AList.find (op =) keylist) keys end; lcp@69: wenzelm@7596: val rev_defs = sort_lhs_depths o map symmetric; lcp@69: skalberg@15570: fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs); wenzelm@7596: fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs)); wenzelm@7596: fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs 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!*) wenzelm@9535: fun rename_params_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@16425: | NONE => paulson@13559: (if !Logic.auto_rename wenzelm@16425: then (warning "Resetting Logic.auto_rename"; wenzelm@16425: Logic.auto_rename := false) wenzelm@16425: else (); PRIMITIVE (rename_params_rule (xs, i))); wenzelm@9535: wenzelm@10817: fun rename_tac str i = wenzelm@10817: let val cs = Symbol.explode str in wenzelm@4693: case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of wenzelm@9535: [] => rename_params_tac (scanwords Symbol.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. *) wenzelm@10817: 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: paulson@2043: (*Prunes all redundant parameters from the proof state by rewriting. paulson@2043: DOES NOT rewrite main goal, where quantification over an unused bound paulson@2043: variable is sometimes done to avoid the need for cut_facts_tac.*) paulson@2043: val prune_params_tac = rewrite_goals_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.*) paulson@2672: fun rotate_tac 0 i = all_tac paulson@2672: | rotate_tac k i = PRIMITIVE (rotate_rule k i); nipkow@1209: paulson@7248: (*Rotates the given subgoal to be the last.*) paulson@7248: fun defer_tac i = PRIMITIVE (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'); nipkow@5974: fun thins ((tac,n),H) = 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 skalberg@15570: in case fst(Library.foldl thins ((NONE,0),Hs)) of skalberg@15531: NONE => no_tac | SOME tac => tac n nipkow@5974: end) nipkow@5974: end; nipkow@5974: wenzelm@11961: wenzelm@12139: (*meta-level conjunction*) wenzelm@12139: val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $ wenzelm@12139: (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) => wenzelm@12139: (fn st => wenzelm@12139: compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st) wenzelm@12139: | _ => no_tac); wenzelm@16425: wenzelm@12139: val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac); wenzelm@12139: wenzelm@15874: fun smart_conjunction_tac 0 = assume_tac 1 wenzelm@15874: | smart_conjunction_tac _ = TRY conjunction_tac; wenzelm@15874: wenzelm@12139: wenzelm@12139: wenzelm@15874: (** minimal goal interface for programmed proofs *) wenzelm@11961: wenzelm@16425: fun gen_prove_multi finish_thm thy xs asms props tac = wenzelm@11961: let wenzelm@15874: val prop = Logic.mk_conjunction_list props; wenzelm@11961: val statement = Logic.list_implies (asms, prop); wenzelm@11961: val frees = map Term.dest_Free (Term.term_frees statement); wenzelm@11970: val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees; berghofe@15797: val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees); haftmann@17271: val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; wenzelm@11961: wenzelm@12212: fun err msg = raise ERROR_MESSAGE wenzelm@12212: (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ wenzelm@16425: Sign.string_of_term thy (Term.list_all_free (params, statement))); wenzelm@11961: wenzelm@16425: fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t) wenzelm@11961: handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; wenzelm@11961: wenzelm@11961: val _ = cert_safe statement; wenzelm@11974: val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg; wenzelm@11961: wenzelm@11974: val cparams = map (cert_safe o Free) params; wenzelm@11961: val casms = map cert_safe asms; wenzelm@12801: val prems = map (norm_hhf_rule o Thm.assume) casms; wenzelm@11961: val goal = Drule.mk_triv_goal (cert_safe prop); wenzelm@11961: wenzelm@11961: val goal' = skalberg@15531: (case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed."); wenzelm@11961: val ngoals = Thm.nprems_of goal'; wenzelm@15874: val _ = conditional (ngoals <> 0) (fn () => wenzelm@15874: err ("Proof failed.\n" ^ wenzelm@15874: Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal')) ^ wenzelm@15874: ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!"))); wenzelm@15874: wenzelm@11961: val raw_result = goal' RS Drule.rev_triv_goal; wenzelm@12801: val prop' = prop_of raw_result; wenzelm@17203: val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () => wenzelm@16425: err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')); wenzelm@11961: in wenzelm@15874: Drule.conj_elim_precise (length props) raw_result wenzelm@15874: |> map (fn res => res wenzelm@11961: |> Drule.implies_intr_list casms wenzelm@11974: |> Drule.forall_intr_list cparams ballarin@16325: |> finish_thm fixed_tfrees) wenzelm@11961: end; wenzelm@11961: wenzelm@16425: fun prove_multi_plain thy xs asms prop tac = wenzelm@16425: gen_prove_multi (K norm_hhf_plain) thy xs asms prop tac; wenzelm@16425: fun prove_multi thy xs asms prop tac = ballarin@16325: gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o ballarin@16325: (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule) wenzelm@16425: thy xs asms prop tac; wenzelm@15874: wenzelm@16425: fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac); wenzelm@16425: fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac); wenzelm@11970: clasohm@0: end; paulson@1501: wenzelm@11774: structure BasicTactic: BASIC_TACTIC = Tactic; wenzelm@11774: open BasicTactic;