From 3ad2f03f7dbc922e2c711241146db091d193003d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 24 May 2020 20:44:33 +0200 Subject: new work on elimination tactic --- spartan/theories/Equivalence.thy | 2 +- spartan/theories/Identity.thy | 2 +- spartan/theories/Spartan.thy | 32 ++++++++++++++++++++++++++------ 3 files changed, 28 insertions(+), 8 deletions(-) (limited to 'spartan/theories') 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 \ (id B)" id_right[symmetric]) apply (rewrite to "(id A) \ h" id_left[symmetric]) - by (rule homotopy_transitive) (assumption, typechk) + by (rule homotopy_transitive) (assumption+, typechk) then have "f \ g ~ f \ 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 \../lib/elimination.ML\ \ \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 \ +val ctxt = @{context}; +val typing = @{term "t: \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 +\ + ML_file \../lib/tactics.ML\ method_setup assumptions = @@ -180,25 +195,30 @@ method_setup intro = method_setup intros = \Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\ -method_setup elim = +method_setup elim' = \Scan.option Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\ +method_setup elim = + \Scan.repeat Args.term >> (fn tms => fn ctxt => + SIMPLE_METHOD' (SIDE_CONDS (elim_tac' tms ctxt) ctxt))\ + method elims = elim+ (*This could possibly use additional simplification hints via a simp: modifier*) method_setup typechk = - \Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\ + \Scan.succeed (fn ctxt => SIMPLE_METHOD' ( + SIDE_CONDS (typechk_tac ctxt) ctxt)) + (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\ method_setup rule = \Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD (HEADGOAL (rule_tac ths ctxt)))\ + SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\ method_setup dest = \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)))\ + SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\ subsection \Rewriting\ -- cgit v1.2.3