From 12eed8685674b7d5ff7bc45a44a061e01f99ce5f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 21 Jul 2020 02:09:44 +0200 Subject: 1. Type-checking/inference now more principled, and the implementation is better. 2. Changed most tactics to context tactics. --- spartan/core/Spartan.thy | 147 +++++++++++++++++++++-------------------------- 1 file changed, 64 insertions(+), 83 deletions(-) (limited to 'spartan/core/Spartan.thy') diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 1b9093b..a4ad300 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -79,16 +79,16 @@ axiomatization lt_trans: "i < j \ j < k \ i < k" axiomatization U :: \lvl \ o\ where - U_hierarchy: "i < j \ U i: U j" and - U_cumulative: "A: U i \ i < j \ A: U j" + Ui_in_Uj: "i < j \ U i: U j" and + in_Uj_if_in_Ui: "A: U i \ i < j \ A: U j" -lemma U_in_U: +lemma Ui_in_USi: "U i: U (S i)" - by (rule U_hierarchy, rule lt_S) + by (rule Ui_in_Uj, rule lt_S) -lemma lift_U: +lemma in_USi_if_in_Ui: "A: U i \ A: U (S i)" - by (erule U_cumulative, rule lt_S) + by (erule in_Uj_if_in_Ui, rule lt_S) subsection \\-type\ @@ -199,70 +199,61 @@ consts "rhs" :: \'a\ ("..") ML_file \congruence.ML\ -subsection \Theorem attributes, type-checking and proof methods\ +subsection \Proof methods and type-checking/inference\ -named_theorems intros and comps +named_theorems form and intro and intros and comp +\ \`intros` stores the introduction rule variants used by the + `intro` and `intros` methods.\ ML_file \elimination.ML\ \ \elimination rules\ ML_file \cases.ML\ \ \case reasoning rules\ lemmas - [intros] = anno PiF PiI SigF SigI and - [elims "?f"] = PiE and - [elims "?p"] = SigE and - [comps] = beta Sig_comp and + [form] = PiF SigF and + [intro] = PiI SigI and + [intros] = PiI[rotated] SigI and + [elim "?f"] = PiE and + [elim "?p"] = SigE and + [comp] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong ML_file \typechecking.ML\ -ML_file \tactics2.ML\ ML_file \tactics.ML\ -method_setup assumptions = - \Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (TRYALL (assumptions_tac ctxt))))\ +method_setup typechk = + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.check_infer)))\ method_setup known = - \Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (TRYALL (known_tac ctxt))))\ + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.known_ctac)))\ + +method_setup rule = + \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ + +method_setup dest = + \Scan.lift (Scan.option (Args.parens Parse.int)) + -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (dest_ctac n_opt ths))))\ method_setup intro = - \Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intro_tac ctxt)))\ + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (intro_ctac))))\ method_setup intros = - \Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\ + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\ method_setup elim = - \Scan.repeat Args.term >> (fn tms => fn ctxt => - CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\ + \Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\ method elims = elim+ method_setup cases = - \Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\ - -(*This could possibly use additional simplification hints via a simp: modifier*) -method_setup typechk' = - \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 (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 (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\ - -(*NEW*) -method_setup typechk = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o Types.check_infer)))\ - -method_setup rule = - \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( - CHEADGOAL o Tactics2.SIDE_CONDS (Tactics2.rule_tac ths))))\ + \Args.term >> (fn tm => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\ subsection \Reflexivity\ @@ -270,14 +261,13 @@ subsection \Reflexivity\ named_theorems refl method refl = (rule refl) -subsection \Trivial proofs modulo typechecking\ +subsection \Trivial proofs (modulo automatic discharge of side conditions)\ method_setup this = - \Scan.succeed (fn ctxt => METHOD ( - EVERY o map (HEADGOAL o - (fn ths => SIDE_CONDS (resolve_tac ctxt ths) ctxt) o - single) - ))\ + \Scan.succeed (K (CONTEXT_METHOD (fn facts => + CHEADGOAL (SIDE_CONDS + (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + facts))))\ subsection \Rewriting\ @@ -298,7 +288,7 @@ lemma eta_expand: lemma rewr_imp: assumes "PROP A \ PROP B" shows "(PROP A \ PROP C) \ (PROP B \ PROP C)" - apply (rule Pure.equal_intr_rule) + apply (Pure.rule Pure.equal_intr_rule) apply (drule equal_elim_rule2[OF assms]; assumption) apply (drule equal_elim_rule1[OF assms]; assumption) done @@ -316,9 +306,11 @@ ML_file \~~/src/HOL/Library/cconv.ML\ ML_file \rewrite.ML\ \ \\reduce\ computes terms via judgmental equalities\ -setup \map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk_tac))\ +setup \map_theory_simpset (fn ctxt => + ctxt addSolver (mk_solver "" (fn ctxt' => + NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\ -method reduce uses add = (simp add: comps add | subst comps)+ +method reduce uses add = changed \((simp add: comp add | sub comp); typechk?)+\ subsection \Implicits\ @@ -387,11 +379,8 @@ lemma refine_codomain: lemma lift_universe_codomain: assumes "A: U i" "f: A \ U j" shows "f: A \ U (S j)" - (*FIXME: Temporary; should be fixed once all methods are rewritten to use - the new typechk*) - apply (Pure.rule refine_codomain, typechk, typechk) - apply (Pure.rule lift_U, typechk) - done + using in_USi_if_in_Ui[of "f {}"] + by (rule refine_codomain) subsection \Function composition\ @@ -413,7 +402,7 @@ lemma funcompI [typechk]: "g \\<^bsub>A\<^esub> f: \x: A. C (f x)" unfolding funcomp_def by typechk -lemma funcomp_assoc [comps]: +lemma funcomp_assoc [comp]: assumes "f: A \ B" "g: B \ C" @@ -423,7 +412,7 @@ lemma funcomp_assoc [comps]: "(h \\<^bsub>B\<^esub> g) \\<^bsub>A\<^esub> f \ h \\<^bsub>A\<^esub> g \\<^bsub>A\<^esub> f" unfolding funcomp_def by reduce -lemma funcomp_lambda_comp [comps]: +lemma funcomp_lambda_comp [comp]: assumes "A: U i" "\x. x: A \ b x: B" @@ -432,7 +421,7 @@ lemma funcomp_lambda_comp [comps]: "(\x: B. c x) \\<^bsub>A\<^esub> (\x: A. b x) \ \x: A. c (b x)" unfolding funcomp_def by reduce -lemma funcomp_apply_comp [comps]: +lemma funcomp_apply_comp [comp]: assumes "f: A \ B" "g: \x: B. C x" "x: A" @@ -454,22 +443,22 @@ abbreviation id where "id A \ \x: A. x" lemma id_type[typechk]: "A: U i \ id A: A \ A" and - id_comp [comps]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ - by reduce + id_comp [comp]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ + by reduce+ -lemma id_left [comps]: +lemma id_left [comp]: assumes "f: A \ B" "A: U i" "B: U i" shows "(id B) \\<^bsub>A\<^esub> f \ f" by (subst eta_exp[of f]) (reduce, rule eta) -lemma id_right [comps]: +lemma id_right [comp]: assumes "f: A \ B" "A: U i" "B: U i" shows "f \\<^bsub>A\<^esub> (id A) \ f" by (subst eta_exp[of f]) (reduce, rule eta) lemma id_U [typechk]: "id (U i): U i \ U i" - by typechk (fact U_in_U) + by typechk (rule Ui_in_USi) (*FIXME: Add annotation rule to typechecker*) section \Pairs\ @@ -482,7 +471,7 @@ lemma fst_type [typechk]: shows "fst A B: (\x: A. B x) \ A" unfolding fst_def by typechk -lemma fst_comp [comps]: +lemma fst_comp [comp]: assumes "a: A" "b: B a" @@ -496,10 +485,10 @@ lemma snd_type [typechk]: shows "snd A B: \p: \x: A. B x. B (fst A B p)" unfolding snd_def by typechk reduce -lemma snd_comp [comps]: +lemma snd_comp [comp]: assumes "a: A" "b: B a" "A: U i" "\x. x: A \ B x: U i" shows "snd A B \ b" - unfolding snd_def by reduce + unfolding snd_def by reduce+ subsection \Notation\ @@ -509,7 +498,7 @@ definition fst_i ("fst") definition snd_i ("snd") where [implicit]: "snd \ Spartan.snd ? ?" -no_translations +translations "fst" \ "CONST Spartan.fst A B" "snd" \ "CONST Spartan.snd A B" @@ -520,22 +509,14 @@ Lemma fst [typechk]: "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "fst p: A" - \ \This can't be solved by a single application of `typechk`; it needs - multiple (two) passes. Something to do with constraint/subgoal reordering.\ - apply (Pure.rule elims) - apply (Pure.rule typechk) - apply known [1] - defer \ \The deferred subgoal is an inhabitation problem.\ - apply known [1] - by known - + by typechk Lemma snd [typechk]: assumes "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "snd p: B (fst p)" - by typechk+ + by typechk method fst for p::o = rule fst[of p] method snd for p::o = rule snd[of p] -- cgit v1.2.3