aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 15:21:02 +0200
committerJosh Chen2020-05-25 15:21:02 +0200
commit3de65af4b59e6d3cc8e74acecf704beccd54b774 (patch)
treee5b7a89c5b22d49915d9266c7aaf27d825ce4271 /spartan
parent3ad2f03f7dbc922e2c711241146db091d193003d (diff)
new elimination tactic
Diffstat (limited to 'spartan')
-rw-r--r--spartan/lib/tactics.ML82
-rw-r--r--spartan/theories/Spartan.thy20
2 files changed, 68 insertions, 34 deletions
diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
index 024abc1..f23bfee 100644
--- a/spartan/lib/tactics.ML
+++ b/spartan/lib/tactics.ML
@@ -16,7 +16,7 @@ val rule_tac: thm list -> Proof.context -> int -> tactic
val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
val intro_tac: Proof.context -> int -> tactic
val intros_tac: Proof.context -> int -> tactic
-val elims_tac: term option -> Proof.context -> int -> tactic
+val old_elims_tac: term option -> Proof.context -> int -> tactic
end *) = struct
@@ -101,7 +101,7 @@ fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
(*Basic elimination tactic, only uses existing type judgments from the context
(performs no type synthesis)*)
-fun elims_tac opt_tm ctxt = case opt_tm of
+fun old_elims_tac opt_tm ctxt = case opt_tm of
NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
| SOME tm => SUBGOAL (fn (goal, i) =>
let
@@ -151,34 +151,82 @@ fun internalize_fact_tac t =
THEN SOMEGOAL (known_tac ctxt)
end)
-fun elim_tac' tms ctxt = case tms of
- [] => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
- | major::_ => SUBGOAL (fn (goal, i) =>
+(*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)
+)
+
+local
+
+fun elim_core_tac tms types ctxt = SUBGOAL (K (
+ 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
+ HEADGOAL (resolve_tac ctxt rules)
+ THEN RANGE (replicate (length tms) (typechk_tac ctxt)) 1
+ end handle Option => no_tac))
+
+in
+
+fun elim_context_tac tms ctxt = case tms of
+ [] => CONTEXT_SUBGOAL (K (Context_Tactic.CONTEXT_TACTIC (HEADGOAL (
+ SIDE_CONDS (eresolve_tac ctxt (map #1 (Elim.rules ctxt))) ctxt))))
+ | major::_ => CONTEXT_SUBGOAL (fn (goal, _) =>
let
- val template = Lib.typing_of_term major
val facts = Proof_Context.facts_of ctxt
val prems = Logic.strip_assums_hyp goal
+ val template = Lib.typing_of_term major
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
in case types of
- [] => no_tac
+ [] => Context_Tactic.CONTEXT_TACTIC no_tac
| _ =>
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)
+ val inserts = map (Thm.prop_of o fst) (Facts.props 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 \<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} i)))
+ ))
+ (*Side conditions*)
+ THEN ALLGOALS (TRY o side_cond_tac ctxt)
in
- resolve_tac ctxt rules i
- THEN RANGE (replicate (length tms) (typechk_tac ctxt)) 1
- end handle Option => no_tac
+ fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT
+ (record_inserts ctxt) (tac st)
+ end
end)
+end
end
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy
index ab2606e..744e219 100644
--- a/spartan/theories/Spartan.thy
+++ b/spartan/theories/Spartan.thy
@@ -165,20 +165,6 @@ lemmas
[comps] = beta Sig_comp and
[cong] = Pi_cong lam_cong Sig_cong
-ML \<open>
-val ctxt = @{context};
-val typing = @{term "t: \<Sum>x: A. B x"};
-val insts = [];
-let
- val (eterm, typing) = Lib.dest_typing typing
- val (rl, tms) = the (Elim.lookup_rule ctxt (Term.head_of typing))
-in
- Drule.infer_instantiate @{context}
- (tms ~~ map (Thm.cterm_of ctxt) (eterm::insts))
- rl
-end
-\<close>
-
ML_file \<open>../lib/tactics.ML\<close>
method_setup assumptions =
@@ -195,13 +181,13 @@ method_setup intro =
method_setup intros =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
-method_setup elim' =
+method_setup old_elim =
\<open>Scan.option Args.term >> (fn tm => fn ctxt =>
- SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\<close>
+ SIMPLE_METHOD' (SIDE_CONDS (old_elims_tac tm ctxt) ctxt))\<close>
method_setup elim =
\<open>Scan.repeat Args.term >> (fn tms => fn ctxt =>
- SIMPLE_METHOD' (SIDE_CONDS (elim_tac' tms ctxt) ctxt))\<close>
+ CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close>
method elims = elim+