aboutsummaryrefslogtreecommitdiff
path: root/spartan/theories
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/theories')
-rw-r--r--spartan/theories/Equivalence.thy2
-rw-r--r--spartan/theories/Identity.thy2
-rw-r--r--spartan/theories/Spartan.thy32
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>