new work on elimination tactic

3 files changed, 28 insertions, 8 deletions

diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy
index 97cd18d..73f1e0d 100644
--- a/spartan/theories/Equivalence.thy
+++ b/spartan/theories/Equivalence.thy
@@ -276,7 +276,7 @@ Lemma (derive) biinv_imp_qinv:
         ultimately have "g ~ h"
           apply (rewrite to "g \<circ> (id B)" id_right[symmetric])
           apply (rewrite to "(id A) \<circ> h" id_left[symmetric])
-          by (rule homotopy_transitive) (assumption, typechk)
+          by (rule homotopy_transitive) (assumption+, typechk)
 
         then have "f \<circ> g ~ f \<circ> h"
           by (rule homotopy_funcomp_right)
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 4a4cc40..3f16f4c 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -40,7 +40,7 @@ axiomatization where
 
 lemmas
   [intros] = IdF IdI and
-  [elims] = IdE and
+  [elims "?p" (*"?x" "?y"*)] = IdE and
   [comps] = Id_comp
 
 
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy
index 5274ea2..ab2606e 100644
--- a/spartan/theories/Spartan.thy
+++ b/spartan/theories/Spartan.thy
@@ -160,10 +160,25 @@ ML_file \<open>../lib/elimination.ML\<close> \<comment> \<open>declares the [eli
 named_theorems intros and comps
 lemmas
   [intros] = PiF PiI SigF SigI and
-  [elims] = PiE SigE and
+  [elims "?f"] = PiE and
+  [elims "?p"] = SigE and
   [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 =
@@ -180,25 +195,30 @@ method_setup intro =
 method_setup intros =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
 
-method_setup elim =
+method_setup elim' =
   \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
     SIMPLE_METHOD' (SIDE_CONDS (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>
+
 method elims = elim+
 
 (*This could possibly use additional simplification hints via a simp: modifier*)
 method_setup typechk =
-  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
-    CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close>
+  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (
+    SIDE_CONDS (typechk_tac ctxt) ctxt))
+    (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\<close>
 
 method_setup rule =
   \<open>Attrib.thms >> (fn ths => fn ctxt =>
-    SIMPLE_METHOD (HEADGOAL (rule_tac ths ctxt)))\<close>
+    SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\<close>
 
 method_setup dest =
   \<open>Scan.lift (Scan.option (Args.parens Parse.int)) -- Attrib.thms
     >> (fn (opt_n, ths) => fn ctxt =>
-        SIMPLE_METHOD (HEADGOAL (dest_tac opt_n ths ctxt)))\<close>
+        SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\<close>
 
 subsection \<open>Rewriting\<close>