diff options
Diffstat (limited to 'mltt/core/tactics.ML')
| -rw-r--r-- | mltt/core/tactics.ML | 180 |
1 files changed, 180 insertions, 0 deletions
diff --git a/mltt/core/tactics.ML b/mltt/core/tactics.ML new file mode 100644 index 0000000..6876d5c --- /dev/null +++ b/mltt/core/tactics.ML @@ -0,0 +1,180 @@ +(* Title: tactics.ML + Author: Joshua Chen + +General tactics for dependent type theory. +*) + +structure Tactics: +sig + +val solve_side_conds: int Config.T +val SIDE_CONDS: int -> context_tactic' -> thm list -> context_tactic' +val rule_ctac: thm list -> context_tactic' +val dest_ctac: int option -> thm list -> context_tactic' +val intro_ctac: context_tactic' +val elim_ctac: term list -> context_tactic' +val cases_ctac: term -> context_tactic' + +end = struct + + +(* Side conditions *) +val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2) + +fun SIDE_CONDS j ctac facts i (cst as (ctxt, st)) = cst |> + (case Config.get ctxt solve_side_conds of + 1 => (ctac CTHEN_ALL_NEW (CTRY o Types.known_ctac facts)) i + | 2 => ctac i CTHEN CREPEAT_IN_RANGE (i + j) (Thm.nprems_of st - i) + (CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts)) + | _ => ctac i) + + +(* rule, dest, intro *) + +local + fun mk_rules _ ths [] = ths + | mk_rules n ths ths' = + let val ths'' = foldr1 (op @) + (map + (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) + ths') + in + mk_rules n (ths @ ths') ths'' + end +in + +(*Resolves with given rules*) +fun rule_ctac ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (resolve_tac ctxt (mk_rules 0 [] ths) i st) + +(*Attempts destruct-resolution with the n-th premise of the given rules*) +fun dest_ctac opt_n ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (dresolve_tac ctxt + (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths) + i st) + +end + +(*Applies an appropriate introduction rule*) +val intro_ctac = CONTEXT_TACTIC' (fn ctxt => SUBGOAL (fn (goal, i) => + let val concl = Logic.strip_assums_concl goal in + if Lib.is_typing concl andalso Lib.is_rigid (Lib.type_of_typing concl) + then resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i + else no_tac + end)) + + +(* Induction/elimination *) + +(*Pushes a known typing t:T into a \<Prod>-type. + This tactic is well-behaved only when t is sufficiently well specified + (otherwise there might be multiple possible judgments t:T that unify, and + which is chosen is undefined).*) +fun internalize_fact_tac t = + Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} => + let + val concl = Logic.strip_assums_concl (Thm.term_of raw_concl) + val C = Lib.type_of_typing concl + val B = Thm.cterm_of ctxt (Lib.lambda_var t C) + val a = Thm.cterm_of ctxt t + (*The resolvent is PiE[where ?B=B and ?a=a]*) + val resolvent = + Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE} + in + HEADGOAL (resolve_tac ctxt [resolvent]) + (*Unify with the correct type T*) + THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac []) + end) + +fun elim_core_tac tms types ctxt = + let + val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types + val rules = flat (map + (fn rule_inst => case rule_inst of + NONE => [] + | SOME (rl, idxnames) => [Drule.infer_instantiate ctxt + (idxnames ~~ map (Thm.cterm_of ctxt) tms) rl]) + rule_insts) + in + resolve_tac ctxt rules + THEN' RANGE (replicate (length tms) (NO_CONTEXT_TACTIC ctxt o Types.check_infer [])) + end handle Option => K no_tac + +(*Premises that have already been pushed into the \<Prod>-type*) +structure Inserts = Proof_Data ( + type T = term Item_Net.T + val init = K (Item_Net.init Term.aconv_untyped single) +) + +fun elim_ctac tms = + case tms of + [] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt))) + | major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) => + let + val facts = map Thm.prop_of (Context_Facts.known ctxt) + val prems = Logic.strip_assums_hyp goal + val template = Lib.typing_of_term major + val types = filter (fn th => Term.could_unify (template, th)) (facts @ prems) + |> map Lib.type_of_typing + in case types of + [] => no_ctac cst + | _ => + let + val inserts = facts @ prems + |> filter Lib.is_typing + |> map Lib.dest_typing + |> filter_out (fn (t, _) => + Term.aconv (t, major) orelse Item_Net.member (Inserts.get ctxt) t) + |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct tms T)) + |> filter (fn (_, i) => i > 0) + (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm. + If they are incomparable, then order by decreasing + `subterm_count_distinct tms T`*) + |> sort (fn (((t1, _), i), ((_, T2), j)) => + Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i))) + |> map (#1 o #1) + val record_inserts = Inserts.map (fold Item_Net.update inserts) + val tac = + (*Push premises having a subterm in `tms` into a \<Prod>*) + fold (fn t => fn tac => + tac THEN HEADGOAL (internalize_fact_tac t ctxt)) + inserts all_tac + (*Apply elimination rule*) + THEN HEADGOAL ( + elim_core_tac tms types ctxt + (*Pull pushed premises back out*) + THEN_ALL_NEW (SUBGOAL (fn (_, i) => + REPEAT_DETERM_N (length inserts) + (resolve_tac ctxt @{thms PiI[rotated]} i)))) + in + TACTIC_CONTEXT (record_inserts ctxt) (tac st) + end + end) + +fun cases_ctac tm = + let fun tac ctxt = + SUBGOAL (fn (goal, i) => + let + val facts = Proof_Context.facts_of ctxt + val prems = Logic.strip_assums_hyp goal + val template = Lib.typing_of_term tm + val types = + map (Thm.prop_of o #1) (Facts.could_unify facts template) + @ filter (fn prem => Term.could_unify (template, prem)) prems + |> map Lib.type_of_typing + val res = (case types of + [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)] + (the (Case.lookup_rule ctxt (Term.head_of typ))) + | [] => raise Option + | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed")) + handle Option => + error ("No case rule known for " ^ (Syntax.string_of_term ctxt tm)) + in + resolve_tac ctxt [res] i + end) + in CONTEXT_TACTIC' tac end + + +end + +open Tactics |