diff options
author | Josh Chen | 2020-07-21 02:16:14 +0200 |
---|---|---|
committer | GitHub | 2020-07-21 02:16:14 +0200 |
commit | dfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (patch) | |
tree | b4c4280b1bc4426059ddd184a2258d15d20a0bab /spartan/core | |
parent | 6aaf4d5b28a5284b3b02fa5c410d2d83a711840b (diff) | |
parent | 12eed8685674b7d5ff7bc45a44a061e01f99ce5f (diff) |
Merge pull request #8 from jaycech3n/dev
Merge big diff on dev
Diffstat (limited to 'spartan/core')
-rw-r--r-- | spartan/core/Spartan.thy | 186 | ||||
-rw-r--r-- | spartan/core/context_tactical.ML | 152 | ||||
-rw-r--r-- | spartan/core/elimination.ML | 6 | ||||
-rw-r--r-- | spartan/core/eqsubst.ML | 36 | ||||
-rw-r--r-- | spartan/core/lib.ML | 3 | ||||
-rw-r--r-- | spartan/core/rewrite.ML | 26 | ||||
-rw-r--r-- | spartan/core/tactics.ML | 285 | ||||
-rw-r--r-- | spartan/core/typechecking.ML | 64 |
8 files changed, 466 insertions, 292 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 8fa6cfe..a4ad300 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -10,22 +10,29 @@ keywords "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and "congruence" "print_coercions" :: thy_decl and "rhs" "derive" "prems" "vars" :: quasi_command - begin section \<open>Prelude\<close> +paragraph \<open>Set up the meta-logic just so.\<close> + +paragraph \<open>Notation.\<close> + declare [[eta_contract=false]] +text \<open> + Rebind notation for meta-lambdas since we want to use `\<lambda>` for the object + lambdas. Meta-functions now use the binder `fn`. +\<close> setup \<open> let val typ = Simple_Syntax.read_typ fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) in Sign.del_syntax (Print_Mode.ASCII, true) - [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))] + [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3))] #> Sign.del_syntax Syntax.mode_default [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))] #> Sign.add_syntax Syntax.mode_default @@ -38,11 +45,16 @@ translations "a $ b" \<rightharpoonup> "a (b)" abbreviation (input) K where "K x \<equiv> fn _. x" +paragraph \<open> + Deeply embed dependent type theory: meta-type of expressions, and typing + judgment. +\<close> + typedecl o judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) -text \<open>Type annotations:\<close> +text \<open>Type annotations for type-checking and inference.\<close> definition anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_ : _')") where "(a : A) \<equiv> a" if "a: A" @@ -51,7 +63,9 @@ lemma anno: "a: A \<Longrightarrow> (a : A): A" by (unfold anno_def) -section \<open>Universes\<close> +section \<open>Axioms\<close> + +subsection \<open>Universes\<close> typedecl lvl \<comment> \<open>Universe levels\<close> @@ -65,19 +79,19 @@ axiomatization lt_trans: "i < j \<Longrightarrow> j < k \<Longrightarrow> i < k" axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where - U_hierarchy: "i < j \<Longrightarrow> U i: U j" and - U_cumulative: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j" + Ui_in_Uj: "i < j \<Longrightarrow> U i: U j" and + in_Uj_if_in_Ui: "A: U i \<Longrightarrow> i < j \<Longrightarrow> 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 \<Longrightarrow> A: U (S i)" - by (erule U_cumulative, rule lt_S) + by (erule in_Uj_if_in_Ui, rule lt_S) -section \<open>\<Prod>-type\<close> +subsection \<open>\<Prod>-type\<close> axiomatization Pi :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and @@ -100,9 +114,9 @@ translations abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" axiomatization where - PiF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and + PiF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and - PiI: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and + PiI: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and PiE: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f `a: B a" and @@ -113,14 +127,14 @@ axiomatization where Pi_cong: "\<lbrakk> \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x; A: U i; - \<And>x. x: A \<Longrightarrow> B x: U i; - \<And>x. x: A \<Longrightarrow> B' x: U i + \<And>x. x: A \<Longrightarrow> B x: U j; + \<And>x. x: A \<Longrightarrow> B' x: U j \<rbrakk> \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. B' x" and lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x" -section \<open>\<Sum>-type\<close> +subsection \<open>\<Sum>-type\<close> axiomatization Sig :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and @@ -138,16 +152,16 @@ abbreviation "and" (infixl "\<and>" 60) where "A \<and> B \<equiv> A \<times> B" axiomatization where - SigF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and + SigF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and SigI: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a, b>: \<Sum>x: A. B x" and SigE: "\<lbrakk> p: \<Sum>x: A. B x; A: U i; - \<And>x. x : A \<Longrightarrow> B x: U i; - \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>; - \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i + \<And>x. x : A \<Longrightarrow> B x: U j; + \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U k; + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y> \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f p: C p" and Sig_comp: "\<lbrakk> @@ -161,22 +175,23 @@ axiomatization where Sig_cong: "\<lbrakk> \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x; A: U i; - \<And>x. x : A \<Longrightarrow> B x: U i; - \<And>x. x : A \<Longrightarrow> B' x: U i + \<And>x. x : A \<Longrightarrow> B x: U j; + \<And>x. x : A \<Longrightarrow> B' x: U j \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x" section \<open>Infrastructure\<close> ML_file \<open>lib.ML\<close> -ML_file \<open>typechecking.ML\<close> +ML_file \<open>context_tactical.ML\<close> subsection \<open>Proof commands\<close> +ML_file \<open>focus.ML\<close> + named_theorems typechk ML_file \<open>goals.ML\<close> -ML_file \<open>focus.ML\<close> subsection \<open>Congruence automation\<close> @@ -184,72 +199,75 @@ consts "rhs" :: \<open>'a\<close> ("..") ML_file \<open>congruence.ML\<close> +subsection \<open>Proof methods and type-checking/inference\<close> + +named_theorems form and intro and intros and comp +\<comment> \<open>`intros` stores the introduction rule variants used by the + `intro` and `intros` methods.\<close> + ML_file \<open>elimination.ML\<close> \<comment> \<open>elimination rules\<close> ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close> -subsection \<open>Methods\<close> - -named_theorems intros and comps lemmas - [intros] = 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 \<open>typechecking.ML\<close> ML_file \<open>tactics.ML\<close> -method_setup assumptions = - \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (TRYALL (assumptions_tac ctxt))))\<close> +method_setup typechk = + \<open>Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.check_infer)))\<close> method_setup known = - \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (TRYALL (known_tac ctxt))))\<close> + \<open>Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.known_ctac)))\<close> + +method_setup rule = + \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close> + +method_setup dest = + \<open>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))))\<close> method_setup intro = - \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intro_tac ctxt)))\<close> + \<open>Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (intro_ctac))))\<close> method_setup intros = - \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close> + \<open>Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\<close> method_setup elim = - \<open>Scan.repeat Args.term >> (fn tms => fn ctxt => - CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close> + \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\<close> method elims = elim+ method_setup cases = - \<open>Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\<close> - -(*This could possibly use additional simplification hints via a simp: modifier*) -method_setup typechk = - \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' ( - SIDE_CONDS (typechk_tac ctxt) ctxt)) - (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\<close> + \<open>Args.term >> (fn tm => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\<close> -method_setup rule = - \<open>Attrib.thms >> (fn ths => fn ctxt => - 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 (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\<close> subsection \<open>Reflexivity\<close> named_theorems refl method refl = (rule refl) -subsection \<open>Trivial proofs modulo typechecking\<close> +subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)\<close> method_setup this = - \<open>Scan.succeed (fn ctxt => METHOD ( - EVERY o map (HEADGOAL o - (fn ths => SIDE_CONDS (resolve_tac ctxt ths) ctxt) o - single) - ))\<close> + \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts => + CHEADGOAL (SIDE_CONDS + (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + facts))))\<close> subsection \<open>Rewriting\<close> @@ -270,7 +288,7 @@ lemma eta_expand: lemma rewr_imp: assumes "PROP A \<equiv> PROP B" shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> 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 @@ -288,9 +306,11 @@ ML_file \<open>~~/src/HOL/Library/cconv.ML\<close> ML_file \<open>rewrite.ML\<close> \<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close> -setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk_tac))\<close> +setup \<open>map_theory_simpset (fn ctxt => + ctxt addSolver (mk_solver "" (fn ctxt' => + NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\<close> -method reduce uses add = (simp add: comps add | subst comps)+ +method reduce uses add = changed \<open>((simp add: comp add | sub comp); typechk?)+\<close> subsection \<open>Implicits\<close> @@ -348,13 +368,19 @@ lemma eta_exp: shows "f \<equiv> \<lambda>x: A. f x" by (rule eta[symmetric]) +lemma refine_codomain: + assumes + "A: U i" + "f: \<Prod>x: A. B x" + "\<And>x. x: A \<Longrightarrow> f `x: C x" + shows "f: \<Prod>x: A. C x" + by (subst eta_exp) + lemma lift_universe_codomain: assumes "A: U i" "f: A \<rightarrow> U j" shows "f: A \<rightarrow> U (S j)" - apply (sub eta_exp) - apply known - apply (Pure.rule intros; rule lift_U) - done + using in_USi_if_in_Ui[of "f {}"] + by (rule refine_codomain) subsection \<open>Function composition\<close> @@ -376,7 +402,7 @@ lemma funcompI [typechk]: "g \<circ>\<^bsub>A\<^esub> f: \<Prod>x: A. C (f x)" unfolding funcomp_def by typechk -lemma funcomp_assoc [comps]: +lemma funcomp_assoc [comp]: assumes "f: A \<rightarrow> B" "g: B \<rightarrow> C" @@ -386,7 +412,7 @@ lemma funcomp_assoc [comps]: "(h \<circ>\<^bsub>B\<^esub> g) \<circ>\<^bsub>A\<^esub> f \<equiv> h \<circ>\<^bsub>A\<^esub> g \<circ>\<^bsub>A\<^esub> f" unfolding funcomp_def by reduce -lemma funcomp_lambda_comp [comps]: +lemma funcomp_lambda_comp [comp]: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> b x: B" @@ -395,7 +421,7 @@ lemma funcomp_lambda_comp [comps]: "(\<lambda>x: B. c x) \<circ>\<^bsub>A\<^esub> (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)" unfolding funcomp_def by reduce -lemma funcomp_apply_comp [comps]: +lemma funcomp_apply_comp [comp]: assumes "f: A \<rightarrow> B" "g: \<Prod>x: B. C x" "x: A" @@ -417,22 +443,22 @@ abbreviation id where "id A \<equiv> \<lambda>x: A. x" lemma id_type[typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and - id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close> - by reduce + id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close> + by reduce+ -lemma id_left [comps]: +lemma id_left [comp]: assumes "f: A \<rightarrow> B" "A: U i" "B: U i" shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f" by (subst eta_exp[of f]) (reduce, rule eta) -lemma id_right [comps]: +lemma id_right [comp]: assumes "f: A \<rightarrow> B" "A: U i" "B: U i" shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f" by (subst eta_exp[of f]) (reduce, rule eta) lemma id_U [typechk]: "id (U i): U i \<rightarrow> U i" - by typechk (fact U_in_U) + by typechk (rule Ui_in_USi) (*FIXME: Add annotation rule to typechecker*) section \<open>Pairs\<close> @@ -445,7 +471,7 @@ lemma fst_type [typechk]: shows "fst A B: (\<Sum>x: A. B x) \<rightarrow> A" unfolding fst_def by typechk -lemma fst_comp [comps]: +lemma fst_comp [comp]: assumes "a: A" "b: B a" @@ -459,10 +485,10 @@ lemma snd_type [typechk]: shows "snd A B: \<Prod>p: \<Sum>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" "\<And>x. x: A \<Longrightarrow> B x: U i" shows "snd A B <a, b> \<equiv> b" - unfolding snd_def by reduce + unfolding snd_def by reduce+ subsection \<open>Notation\<close> @@ -483,7 +509,7 @@ Lemma fst [typechk]: "p: \<Sum>x: A. B x" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" shows "fst p: A" - by typechk + by typechk Lemma snd [typechk]: assumes diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML new file mode 100644 index 0000000..a5159f6 --- /dev/null +++ b/spartan/core/context_tactical.ML @@ -0,0 +1,152 @@ +(* Title: context_tactical.ML + Author: Joshua Chen + +More context tactics, and context tactic combinators. +*) + +infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD +infix 0 CORELSE CAPPEND CORELSE' CAPPEND' + +structure Context_Tactical: +sig + +type context_tactic' = int -> context_tactic +val CONTEXT_TACTIC': (Proof.context -> int -> tactic) -> context_tactic' +val all_ctac: context_tactic +val no_ctac: context_tactic +val print_ctac: (Proof.context -> string) -> context_tactic +val CTHEN: context_tactic * context_tactic -> context_tactic +val CORELSE: context_tactic * context_tactic -> context_tactic +val CAPPEND: context_tactic * context_tactic -> context_tactic +val CTHEN': context_tactic' * context_tactic' -> context_tactic' +val CORELSE': context_tactic' * context_tactic' -> context_tactic' +val CAPPEND': context_tactic' * context_tactic' -> context_tactic' +val CTRY: context_tactic -> context_tactic +val CREPEAT: context_tactic -> context_tactic +val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic +val CCHANGED: context_tactic -> context_tactic +val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic' +val CREPEAT_IN_RANGE: int -> int -> context_tactic' -> context_tactic +val CREPEAT_ALL_NEW: context_tactic' -> context_tactic' +val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic' +val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic' +val CHEADGOAL: context_tactic' -> context_tactic +val CALLGOALS: context_tactic' -> context_tactic +val CSOMEGOAL: context_tactic' -> context_tactic +val CRANGE: context_tactic' list -> context_tactic' + +end = struct + +type context_tactic' = int -> context_tactic + +fun CONTEXT_TACTIC' tac i (ctxt, st) = TACTIC_CONTEXT ctxt ((tac ctxt i) st) + +val all_ctac = Seq.make_results o Seq.single +val no_ctac = K Seq.empty +fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st) + +fun (ctac1 CTHEN ctac2) cst = Seq.maps_results ctac2 (ctac1 cst) + +fun (ctac1 CORELSE ctac2) cst = + (case Seq.pull (ctac1 cst) of + NONE => ctac2 cst + | some => Seq.make (fn () => some)) + +fun (ctac1 CAPPEND ctac2) cst = + Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst))) + +fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x +fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x +fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x + +fun CTRY ctac = ctac CORELSE all_ctac + +fun CREPEAT ctac = + let + fun rep qs cst = + (case Seq.pull (Seq.filter_results (ctac cst)) of + NONE => SOME (cst, Seq.make (fn () => repq qs)) + | SOME (cst', q) => rep (q :: qs) cst') + and repq [] = NONE + | repq (q :: qs) = + (case Seq.pull q of + NONE => repq qs + | SOME (cst, q) => rep (q :: qs) cst); + in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end + +fun CFILTER pred ctac cst = + ctac cst + |> Seq.filter_results + |> Seq.filter pred + |> Seq.make_results + +(*Only accept next states where the subgoals have changed*) +fun CCHANGED ctac (cst as (_, st)) = + CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst + +local + fun op THEN (f, g) x = Seq.maps_results g (f x) + + fun INTERVAL f i j x = + if i > j then Seq.make_results (Seq.single x) + else op THEN (f j, INTERVAL f i (j - 1)) x + + (*By Peter Lammich: apply tactic to subgoals in interval in a forward manner, + skipping over emerging subgoals*) + fun INTERVAL_FWD ctac l u (cst as (_, st)) = cst |> + (if l > u then all_ctac + else (ctac l CTHEN (fn cst' as (_, st') => + let val ofs = Thm.nprems_of st' - Thm.nprems_of st in + if ofs < ~1 + then raise THM ( + "INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st']) + else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst' + end))) +in + +fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) = + cst |> (ctac1 i CTHEN (fn cst' as (_, st') => + INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst')) + +(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward + manner*) +fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) = + cst |> (ctac1 i CTHEN (fn cst' as (_, st') => + INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst')) + +(*Repeatedly apply ctac to the i-th until the k-th-from-last subgoals + (i.e. leave the last k subgoals alone), until no more changes appear in the + goal state.*) +fun CREPEAT_IN_RANGE i k ctac = + let fun interval_ctac (cst as (_, st)) = + INTERVAL_FWD ctac i (Thm.nprems_of st - k) cst + in CREPEAT (CCHANGED interval_ctac) end + +end + +fun CREPEAT_ALL_NEW ctac = + ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i)) + +fun CREPEAT_ALL_NEW_FWD ctac = + ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i)) + +fun CHEADGOAL ctac = ctac 1 + +fun CALLGOALS ctac (cst as (_, st)) = + let + fun doall 0 = all_ctac + | doall n = ctac n CTHEN doall (n - 1); + in doall (Thm.nprems_of st) cst end + +fun CSOMEGOAL ctac (cst as (_, st)) = + let + fun find 0 = no_ctac + | find n = ctac n CORELSE find (n - 1); + in find (Thm.nprems_of st) cst end + +fun CRANGE [] _ = all_ctac + | CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i + +end + +open Context_Tactical diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML index 11b3af9..cd4e414 100644 --- a/spartan/core/elimination.ML +++ b/spartan/core/elimination.ML @@ -34,13 +34,13 @@ fun register_rule tms rl = in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end -(* [elims] attribute *) +(* [elim] attribute *) val _ = Theory.setup ( - Attrib.setup \<^binding>\<open>elims\<close> + Attrib.setup \<^binding>\<open>elim\<close> (Scan.repeat Args.term_pattern >> (Thm.declaration_attribute o register_rule)) "" - #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>, + #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elim\<close>, fn context => (map #1 (rules (Context.proof_of context)))) ) diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML index ea6f098..e7ecf63 100644 --- a/spartan/core/eqsubst.ML +++ b/spartan/core/eqsubst.ML @@ -416,19 +416,27 @@ fun eqsubst_asm_tac ctxt occs thms i st = should be done to an assumption, false = apply to the conclusion of the goal) as well as the theorems to use *) val _ = - Theory.setup - (Method.setup \<^binding>\<open>sub\<close> - (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- - Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt => - SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) - "single-step substitution" - #> - (Method.setup \<^binding>\<open>subst\<close> - (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- - Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt => - SIMPLE_METHOD' (SIDE_CONDS - ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms) - ctxt))) - "single-step substitution with auto-typechecking")) + let + val parser = + Scan.lift (Args.mode "asm" + -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) + -- Attrib.thms + fun eqsubst_asm_ctac occs inthms = + CONTEXT_TACTIC' (fn ctxt => eqsubst_asm_tac ctxt occs inthms) + fun eqsubst_ctac occs inthms = + CONTEXT_TACTIC' (fn ctxt => eqsubst_tac ctxt occs inthms) + in + Theory.setup ( + Method.setup \<^binding>\<open>sub\<close> + (parser >> (fn ((asm, occs), inthms) => fn ctxt => SIMPLE_METHOD' ( + (if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) + "single-step substitution" #> + Method.setup \<^binding>\<open>subst\<close> + (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS + ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms))))) + "single-step substitution with automatic discharge of side conditions" + ) + end end; diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML index 615f601..7b93a08 100644 --- a/spartan/core/lib.ML +++ b/spartan/core/lib.ML @@ -7,6 +7,7 @@ val maxint: int list -> int (*Terms*) val is_rigid: term -> bool +val no_vars: term -> bool val dest_eq: term -> term * term val mk_Var: string -> int -> typ -> term val lambda_var: term -> term -> term @@ -50,6 +51,8 @@ val maxint = max (op >) val is_rigid = not o is_Var o head_of +val no_vars = not o exists_subterm is_Var + fun dest_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ def) = (t, def) | dest_eq _ = error "dest_eq" diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index f9c5d8e..eba0e81 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -15,8 +15,8 @@ patterns but has diverged significantly during its development. We also allow introduction of identifiers for bound variables, which can then be used to match arbitrary subterms inside abstractions. -This code is slightly modified from the original at HOL/Library/rewrite.ML, -to incorporate auto-typechecking for type theory. +This code has been slightly modified from the original at HOL/Library/rewrite.ML +to incorporate automatic discharge of type-theoretic side conditions. *) infix 1 then_pconv; @@ -448,18 +448,18 @@ val _ = val subst_parser = let val scan = raw_pattern -- to_parser -- Parse.thms1 in context_lift scan prep_args end + + fun rewrite_export_ctac inputs inthms = + CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms) in Method.setup \<^binding>\<open>rewr\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) - "single-step rewriting, allowing subterm selection via patterns" - #> - (Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' (SIDE_CONDS - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms) - orig_ctxt))) - "single-step rewriting with auto-typechecking") + (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD' + (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) + "single-step rewriting, allowing subterm selection via patterns" #> + Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> + (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS + (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) + "single-step rewriting with auto-typechecking" end end diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 0c71665..3922ae0 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -7,109 +7,66 @@ General tactics for dependent type theory. structure Tactics: sig -val assumptions_tac: Proof.context -> int -> tactic -val known_tac: Proof.context -> int -> tactic -val typechk_tac: Proof.context -> int -> tactic -val auto_typechk: bool Config.T -val SIDE_CONDS: (int -> tactic) -> Proof.context -> int -> tactic -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 elim_context_tac: term list -> Proof.context -> int -> context_tactic -val cases_tac: term -> Proof.context -> int -> tactic +val solve_side_conds: int Config.T +val SIDE_CONDS: context_tactic' -> thm list -> context_tactic' +val rule_ctac: thm list -> context_tactic' +val dest_ctac: int option -> thm list -> context_tactic' +val intro_ctac: context_tactic' +val elim_ctac: term list -> context_tactic' +val cases_ctac: term -> context_tactic' end = struct -(*An assumption tactic that only solves typing goals with rigid terms and - judgmental equalities without schematic variables*) -fun assumptions_tac ctxt = SUBGOAL (fn (goal, i) => - let - val concl = Logic.strip_assums_concl goal - in - if - Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl) - orelse not ((exists_subterm is_Var) concl) - then assume_tac ctxt i - else no_tac - end) - -(*Solves typing goals with rigid term by resolving with context facts and - simplifier premises, or arbitrary goals by *non-unifying* assumption*) -fun known_tac ctxt = SUBGOAL (fn (goal, i) => - let - val concl = Logic.strip_assums_concl goal - in - ((if Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl) - then - let val ths = map fst (Facts.props (Proof_Context.facts_of ctxt)) - in resolve_tac ctxt (ths @ Simplifier.prems_of ctxt) end - else K no_tac) - ORELSE' assumptions_tac ctxt) i - end) - -(*Typechecking: try to solve goals of the form "a: A" where a is rigid*) -fun typechk_tac ctxt = - let - val tac = SUBGOAL (fn (goal, i) => - if Lib.rigid_typing_concl goal - then - let val net = Tactic.build_net - ((Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>) - @(Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>) - @(map #1 (Elim.rules ctxt))) - in (resolve_from_net_tac ctxt net) i end - else no_tac) - in - REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac) - end -fun typechk_context_tac (ctxt, st) = - let - - in - () - end +(* Side conditions *) +val solve_side_conds = + Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2) -(*Many methods try to automatically discharge side conditions by typechecking. - Switch this flag off to discharge by non-unifying assumption instead.*) -val auto_typechk = Attrib.setup_config_bool \<^binding>\<open>auto_typechk\<close> (K true) +fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN + (case Config.get ctxt solve_side_conds of + 1 => CALLGOALS (CTRY o Types.known_ctac facts) + | 2 => CREPEAT_IN_RANGE i (Thm.nprems_of st - i) + (CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts)) + | _ => all_ctac)) -fun side_cond_tac ctxt = CHANGED o REPEAT o - (if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt) -(*Combinator runs tactic and tries to discharge all new typing side conditions*) -fun SIDE_CONDS tac ctxt = tac THEN_ALL_NEW (TRY o side_cond_tac ctxt) +(* rule, dest, intro *) local -fun mk_rules _ ths [] = ths - | mk_rules n ths ths' = - let val ths'' = foldr1 (op @) - (map (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) ths') - in - mk_rules n (ths @ ths') ths'' - end + fun mk_rules _ ths [] = ths + | mk_rules n ths ths' = + let val ths'' = foldr1 (op @) + (map + (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) + ths') + in + mk_rules n (ths @ ths') ths'' + end in -(*Resolves with given rules, discharging as many side conditions as possible*) -fun rule_tac ths ctxt = resolve_tac ctxt (mk_rules 0 [] ths) +(*Resolves with given rules*) +fun rule_ctac ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (resolve_tac ctxt (mk_rules 0 [] ths) i st) (*Attempts destruct-resolution with the n-th premise of the given rules*) -fun dest_tac opt_n ths ctxt = dresolve_tac ctxt - (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths) +fun dest_ctac opt_n ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (dresolve_tac ctxt + (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths) + i st) end (*Applies some introduction rule*) -fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS - (resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)) ctxt i) +fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt + (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>) i st) -fun intros_tac ctxt = SUBGOAL (fn (_, i) => - (CHANGED o REPEAT o CHANGED o intro_tac ctxt) i) (* Induction/elimination *) -(*Pushes a context/goal premise typing t:T into a \<Prod>-type*) +(*Pushes a known typing t:T into a \<Prod>-type. + This tactic is well-behaved only when t is sufficiently well specified + (otherwise there might be multiple possible judgments t:T that unify, and + which is chosen is undefined).*) fun internalize_fact_tac t = Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} => let @@ -123,18 +80,10 @@ fun internalize_fact_tac t = in HEADGOAL (resolve_tac ctxt [resolvent]) (*known_tac infers the correct type T inferred by unification*) - THEN SOMEGOAL (known_tac ctxt) + THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac []) end) -(*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 ( +fun elim_core_tac tms types ctxt = let val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types val rules = flat (map @@ -144,84 +93,86 @@ fun elim_core_tac tms types ctxt = SUBGOAL (K ( (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)) + resolve_tac ctxt rules + THEN' RANGE (replicate (length tms) (NO_CONTEXT_TACTIC ctxt o Types.check_infer [])) + end handle Option => K 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 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 - [] => Context_Tactic.CONTEXT_TACTIC no_tac - | _ => - let - 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 - fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT - (record_inserts ctxt) (tac st) - end - end) +(*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) +) -fun cases_tac tm ctxt = SUBGOAL (fn (goal, i) => - let - val facts = Proof_Context.facts_of ctxt - val prems = Logic.strip_assums_hyp goal - val template = Lib.typing_of_term tm - 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 - val res = (case types of - [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)] - (the (Case.lookup_rule ctxt (Term.head_of typ))) - | [] => raise Option - | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed")) - handle Option => error ("no case rule known for " - ^ (Syntax.string_of_term ctxt tm)) - in - SIDE_CONDS (resolve_tac ctxt [res]) ctxt i - end) +fun elim_ctac tms = + case tms of + [] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt))) + | major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) => + let + 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_ctac cst + | _ => + let + 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[rotated]} i)))) + in + TACTIC_CONTEXT (record_inserts ctxt) (tac st) + end + end) + +fun cases_ctac tm = + let fun tac ctxt = + SUBGOAL (fn (goal, i) => + let + val facts = Proof_Context.facts_of ctxt + val prems = Logic.strip_assums_hyp goal + val template = Lib.typing_of_term tm + 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 + val res = (case types of + [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)] + (the (Case.lookup_rule ctxt (Term.head_of typ))) + | [] => raise Option + | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed")) + handle Option => + error ("no case rule known for " ^ (Syntax.string_of_term ctxt tm)) + in + resolve_tac ctxt [res] i + end) + in CONTEXT_TACTIC' tac end -end end diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index 437a2dc..946ecd6 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -1,7 +1,7 @@ (* Title: typechecking.ML Author: Joshua Chen -Type information and typechecking infrastructure. +Type information and type-checking infrastructure. *) structure Types: sig @@ -11,11 +11,12 @@ val types: Proof.context -> term -> thm list val put_type: thm -> Proof.context -> Proof.context val put_types: thm list -> Proof.context -> Proof.context -val check: Proof.context -> thm -> int -> tactic -val infer: Proof.context -> thm -> int -> tactic +val known_ctac: thm list -> int -> context_tactic +val check_infer: thm list -> int -> context_tactic end = struct + (* Context data *) structure Data = Generic_Data ( @@ -32,22 +33,55 @@ fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing)) fun put_types typings = foldr1 (op o) (map put_type typings) -(* Checking and inference *) - +(* Context tactics for type-checking *) + +(*Solves goals without metavariables and type inference problems by resolving + with facts or assumption from inline premises.*) +fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => + TACTIC_CONTEXT ctxt + let val concl = Logic.strip_assums_concl goal in + if Lib.no_vars concl orelse + (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl)) + then + let val ths = facts + (*FIXME: Shouldn't pull nameless facts directly from context*) + @ map fst (Facts.props (Proof_Context.facts_of ctxt)) + in (resolve_tac ctxt ths i ORELSE assume_tac ctxt i) st end + else Seq.empty + end) + +(*Simple bidirectional typing tactic, with some nondeterminism from backtracking + search over arbitrary `typechk` rules. The current implementation does not + perform any normalization.*) local - -fun checkable prop = Lib.is_typing prop - andalso not (exists_subterm is_Var (Lib.type_of_typing prop)) - + fun check_infer_step facts i (ctxt, st) = + let + val tac = SUBGOAL (fn (goal, i) => + if Lib.rigid_typing_concl goal + then + let val net = Tactic.build_net (facts + (*MAYBE FIXME: Remove `typechk` from this list, and instead perform + definitional unfolding to (w?)hnf.*) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) + @(map #1 (Elim.rules ctxt))) + in (resolve_from_net_tac ctxt net) i end + else no_tac) + val ctxt' = ctxt + in + TACTIC_CONTEXT ctxt' (tac i st) + end in -fun check ctxt rule = Subgoal.FOCUS_PREMS ( - fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt - -fun infer ctxt rule = Subgoal.FOCUS_PREMS ( - fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt +fun check_infer facts i (cst as (_, st)) = + let + val ctac = known_ctac facts CORELSE' check_infer_step facts + in + cst |> (ctac i CTHEN + CREPEAT_IN_RANGE i (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD ctac)) + end end - end |