From 2feb56660700af107abb5a28a7120052ac405518 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 31 Jan 2021 02:54:51 +0000 Subject: rename things + some small changes --- spartan/core/tactics.ML | 180 ------------------------------------------------ 1 file changed, 180 deletions(-) delete mode 100644 spartan/core/tactics.ML (limited to 'spartan/core/tactics.ML') diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML deleted file mode 100644 index 923a3a7..0000000 --- a/spartan/core/tactics.ML +++ /dev/null @@ -1,180 +0,0 @@ -(* 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>\solve_side_conds\ (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>\intro\) i - else no_tac - end)) - - -(* Induction/elimination *) - -(*Pushes a known typing t:T into a \-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 \-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 [p, x, y] 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 \*) - 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 -- cgit v1.2.3