aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--hott/Equivalence.thy48
-rw-r--r--hott/Identity.thy47
-rw-r--r--hott/List+.thy4
-rw-r--r--spartan/core/Spartan.thy72
-rw-r--r--spartan/core/eqsubst.ML4
-rw-r--r--spartan/core/types.ML57
6 files changed, 114 insertions, 118 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index a57ed44..99300a0 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -144,8 +144,6 @@ Lemma (def) commute_homotopy:
apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp)
by refl
-\<comment> \<open>TODO: *Really* need normalization during type-checking and better equality
- type rewriting to do the proof below properly\<close>
Corollary (def) commute_homotopy':
assumes
"A: U i"
@@ -154,21 +152,18 @@ Corollary (def) commute_homotopy':
"H: f ~ (id A)"
shows "H (f x) = f [H x]"
proof -
+ (*FIXME: Bug; if the following type declaration isn't made then bad things
+ happen on the next lines.*)
from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
by (reduce add: homotopy_def)
- have *: "(id A)[H x]: f x = x"
- by (rewrite at "\<hole> = _" id_comp[symmetric],
- rewrite at "_ = \<hole>" id_comp[symmetric])
-
have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
- by (rule left_whisker, fact *, transport eq: ap_id) (reduce+, refl)
+ by (rule left_whisker, transport eq: ap_id, refl)
also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
by (rule commute_homotopy)
- finally have *: "{}" using * by this
+ finally have "{}" by this
- show "H (f x) = f [H x]"
- by pathcomp_cancelr (fact, typechk+)
+ thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+)
qed
@@ -309,23 +304,11 @@ Lemma (def) is_qinv_if_is_biinv:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "is_biinv f \<rightarrow> is_qinv f"
apply intro
-
- text \<open>Split the hypothesis \<^term>\<open>is_biinv f\<close> into its components and name them.\<close>
unfolding is_biinv_def apply elims
focus vars _ _ _ g H1 h H2
- text \<open>Need to give the required function and homotopies.\<close>
apply (rule is_qinvI)
- text \<open>We claim that \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>.\<close>
\<^item> by (fact \<open>g: _\<close>)
-
- text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close>
\<^item> by (fact \<open>H1: _\<close>)
-
- text \<open>
- It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>,
- then the result follows from @{thm \<open>H2: f \<circ> h ~ id B\<close>}. Here a proof
- block is used for calculational reasoning.
- \<close>
\<^item> proof -
have "g ~ g \<circ> (id B)" by reduce refl
also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric])
@@ -437,7 +420,7 @@ Lemma (def) equiv_if_equal:
by (rule lift_universe_codomain, rule Ui_in_USi)
\<^enum> vars A
using [[solve_side_conds=1]]
- apply (subst transport_comp)
+ apply (rewrite transport_comp)
\<circ> by (rule Ui_in_USi)
\<circ> by reduce (rule in_USi_if_in_Ui)
\<circ> by reduce (rule id_is_biinv)
@@ -452,24 +435,5 @@ Lemma (def) equiv_if_equal:
by (rule lift_universe_codomain, rule Ui_in_USi)
done
-(*Uncomment this to see all implicits from here on.
-no_translations
- "f x" \<leftharpoondown> "f `x"
- "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y"
- "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
- "p\<inverse>" \<leftharpoondown> "CONST pathinv A x y p"
- "p \<bullet> q" \<leftharpoondown> "CONST pathcomp A x y z p q"
- "fst" \<leftharpoondown> "CONST Spartan.fst A B"
- "snd" \<leftharpoondown> "CONST Spartan.snd A B"
- "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
- "trans P p" \<leftharpoondown> "CONST transport A P x y p"
- "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p"
- "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u"
- "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p"
- "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
- "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f"
- "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f"
-*)
-
end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 247d6a4..dc27ee8 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -242,7 +242,7 @@ Lemma (def) ap_funcomp:
"x: A" "y: A"
"f: A \<rightarrow> B" "g: B \<rightarrow> C"
"p: x = y"
- shows "(g \<circ> f)[p] = g[f[p]]" thm ap
+ shows "(g \<circ> f)[p] = g[f[p]]"
apply (eq p)
\<^item> by reduce
\<^item> by reduce refl
@@ -251,10 +251,7 @@ Lemma (def) ap_funcomp:
Lemma (def) ap_id:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "(id A)[p] = p"
- apply (eq p)
- \<^item> by reduce
- \<^item> by reduce refl
- done
+ by (eq p) (reduce, refl)
section \<open>Transport\<close>
@@ -303,7 +300,7 @@ Lemma (def) pathcomp_cancel_left:
by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl
also have ".. = p\<inverse> \<bullet> (p \<bullet> r)"
by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl
- also have ".. = r" thm inv_pathcomp
+ also have ".. = r"
by (transport eq: pathcomp_assoc,
transport eq: inv_pathcomp,
transport eq: refl_pathcomp) refl
@@ -339,7 +336,7 @@ Lemma (def) transport_left_inv:
"x: A" "y: A"
"p: x = y"
shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
- by (eq p) (reduce; refl)
+ by (eq p) (reduce, refl)
Lemma (def) transport_right_inv:
assumes
@@ -440,10 +437,7 @@ Lemma (def) pathlift_fst:
"u: P x"
"p: x = y"
shows "fst[lift P p u] = p"
- apply (eq p)
- \<^item> by reduce
- \<^item> by reduce refl
- done
+ by (eq p) (reduce, refl)
section \<open>Dependent paths\<close>
@@ -585,10 +579,10 @@ end
section \<open>Loop space\<close>
definition \<Omega> where "\<Omega> A a \<equiv> a =\<^bsub>A\<^esub> a"
-definition \<Omega>2 where "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)"
+definition \<Omega>2 where "\<Omega>2 A a \<equiv> refl a =\<^bsub>a =\<^bsub>A\<^esub> a\<^esub> refl a"
-Lemma \<Omega>2_alt_def:
- "\<Omega>2 A a \<equiv> refl a = refl a"
+Lemma \<Omega>2_\<Omega>_of_\<Omega>:
+ "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)"
unfolding \<Omega>2_def \<Omega>_def .
@@ -604,23 +598,20 @@ interpretation \<Omega>2:
notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
-Lemma [type]:
+Lemma
assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a"
- shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a"
- and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
+ shows horiz_pathcomp_type [type]: "\<alpha> \<star> \<beta>: \<Omega>2 A a"
+ and horiz_pathcomp'_type [type]: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
using assms
- unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_alt_def
+ unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_def
by reduce+
Lemma (def) pathcomp_eq_horiz_pathcomp:
assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
unfolding \<Omega>2.horiz_pathcomp_def
- (*FIXME: Definitional unfolding + normalization; shouldn't need explicit
- unfolding*)
- using assms[unfolded \<Omega>2_alt_def, type]
+ using assms[unfolded \<Omega>2_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*)
proof (reduce, rule pathinv)
- \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
by (rule pathcomp_refl)
also have ".. = \<alpha>" by (rule refl_pathcomp)
@@ -641,7 +632,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
unfolding \<Omega>2.horiz_pathcomp'_def
- using assms[unfolded \<Omega>2_alt_def, type]
+ using assms[unfolded \<Omega>2_def, type]
proof reduce
have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
by (rule pathcomp_refl)
@@ -662,20 +653,18 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
Lemma (def) eckmann_hilton:
assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
- using assms[unfolded \<Omega>2_alt_def, type]
+ using \<Omega>2_def[comp]
proof -
have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
by (rule pathcomp_eq_horiz_pathcomp)
also have [simplified comp]: ".. = \<alpha> \<star>' \<beta>"
- \<comment> \<open>Danger, Will Robinson! (Inferred implicit has an equivalent form but
- needs to be manually simplified.)\<close>
+ \<comment> \<open>Danger! Inferred implicit has an equivalent form but needs to be
+ manually simplified.\<close>
by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
also have ".. = \<beta> \<bullet> \<alpha>"
by (rule pathcomp_eq_horiz_pathcomp')
finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
- by (this; reduce add: \<Omega>2_alt_def[symmetric])
- \<comment> \<open>TODO: The finishing call to `reduce` should be unnecessary with some
- kind of definitional unfolding.\<close>
+ by this
qed
end
diff --git a/hott/List+.thy b/hott/List+.thy
index b73cc24..869d667 100644
--- a/hott/List+.thy
+++ b/hott/List+.thy
@@ -10,8 +10,8 @@ section \<open>Length\<close>
definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"
experiment begin
- Lemma "len [] \<equiv> ?n" by (subst comp)
- Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)
+ Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)
+ Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+
end
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 10caa30..6b2ed58 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -181,18 +181,16 @@ axiomatization where
\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
-section \<open>Infrastructure\<close>
+section \<open>Type checking & inference\<close>
ML_file \<open>lib.ML\<close>
ML_file \<open>context_facts.ML\<close>
ML_file \<open>context_tactical.ML\<close>
-subsection \<open>Type-checking/inference\<close>
-
-\<comment> \<open>Rule attributes for the type-checker\<close>
+\<comment> \<open>Rule attributes for the typechecker\<close>
named_theorems form and intr and comp
-\<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
+\<comment> \<open>Elimination/induction automation and the `elim` attribute\<close>
ML_file \<open>elimination.ML\<close>
lemmas
@@ -203,7 +201,20 @@ lemmas
[comp] = beta Sig_comp and
[cong] = Pi_cong lam_cong Sig_cong
-\<comment> \<open>Type-checking\<close>
+\<comment> \<open>Subsumption rule\<close>
+lemma sub:
+ assumes "a: A" "A \<equiv> A'"
+ shows "a: A'"
+ using assms by simp
+
+\<comment> \<open>Basic substitution of definitional equalities\<close>
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
+
+\<comment> \<open>Term normalization, type checking & inference\<close>
ML_file \<open>types.ML\<close>
method_setup typechk =
@@ -214,14 +225,26 @@ method_setup known =
\<open>Scan.succeed (K (CONTEXT_METHOD (
CHEADGOAL o Types.known_ctac)))\<close>
-subsection \<open>Statement commands\<close>
+setup \<open>
+let val typechk = fn ctxt =>
+ NO_CONTEXT_TACTIC ctxt o Types.check_infer
+ (Simplifier.prems_of ctxt @ Context_Facts.known ctxt)
+in
+ map_theory_simpset (fn ctxt => ctxt
+ addSolver (mk_solver "" typechk))
+end
+\<close>
+
+
+section \<open>Statements and goals\<close>
ML_file \<open>focus.ML\<close>
ML_file \<open>elaboration.ML\<close>
ML_file \<open>elaborated_statement.ML\<close>
ML_file \<open>goals.ML\<close>
-subsection \<open>Proof methods\<close>
+
+section \<open>Proof methods\<close>
named_theorems intro \<comment> \<open>Logical introduction rules\<close>
@@ -270,6 +293,7 @@ subsection \<open>Reflexivity\<close>
named_theorems refl
method refl = (rule refl)
+
subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)\<close>
method_setup this =
@@ -278,16 +302,9 @@ method_setup this =
(CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
facts))))\<close>
-subsection \<open>Rewriting\<close>
-\<comment> \<open>\<open>subst\<close> method\<close>
-ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
-ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
-ML_file \<open>eqsubst.ML\<close>
+subsection \<open>Rewriting\<close>
-\<comment> \<open>\<open>rewrite\<close> method\<close>
consts rewrite_HOLE :: "'a::{}" ("\<hole>")
lemma eta_expand:
@@ -315,20 +332,18 @@ 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 "" (fn ctxt' =>
- NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\<close>
-
method reduce uses add =
- changed \<open>repeat_new \<open>(simp add: comp add | sub comp); typechk?\<close>\<close>
+ changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
-subsection \<open>Congruence automation\<close>
+
+subsection \<open>Congruence relations\<close>
consts "rhs" :: \<open>'a\<close> ("..")
ML_file \<open>congruence.ML\<close>
-subsection \<open>Implicits\<close>
+
+section \<open>Implicits\<close>
text \<open>
\<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
@@ -364,7 +379,8 @@ translations
translations "\<lambda>x. b" \<leftharpoondown> "\<lambda>x: A. b"
-subsection \<open>Lambda coercion\<close>
+
+section \<open>Lambda coercion\<close>
\<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
@@ -389,7 +405,7 @@ Lemma refine_codomain:
"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)
+ by (rewrite eta_exp)
Lemma lift_universe_codomain:
assumes "A: U i" "f: A \<rightarrow> U j"
@@ -463,12 +479,12 @@ lemma
Lemma id_left [comp]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
- by (subst eta_exp[of f]) (reduce, rule eta)
+ by (rewrite eta_exp[of f]) (reduce, rule eta)
Lemma id_right [comp]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
- by (subst eta_exp[of f]) (reduce, rule eta)
+ by (rewrite eta_exp[of f]) (reduce, rule eta)
lemma id_U [type]:
"id (U i): U i \<rightarrow> U i"
@@ -494,7 +510,7 @@ Lemma fst_comp [comp]:
Lemma snd_type [type]:
assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
shows "snd A B: \<Prod>p: \<Sum>x: A. B x. B (fst A B p)"
- unfolding snd_def by typechk reduce
+ unfolding snd_def by typechk
Lemma snd_comp [comp]:
assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML
index 31d5126..5ae8c73 100644
--- a/spartan/core/eqsubst.ML
+++ b/spartan/core/eqsubst.ML
@@ -430,12 +430,12 @@ val _ =
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" #>
+ "single-step substitution" (* #>
Method.setup \<^binding>\<open>subst\<close>
(parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD (
CHEADGOAL o SIDE_CONDS 0
((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms)))))
- "single-step substitution with automatic discharge of side conditions"
+ "single-step substitution with automatic discharge of side conditions" *)
)
end
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
index 70e5057..67918b9 100644
--- a/spartan/core/types.ML
+++ b/spartan/core/types.ML
@@ -43,42 +43,69 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
if Lib.no_vars concl orelse
(Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
then
- let val ths = known ctxt @ map (Simplifier.norm_hhf ctxt) facts
+ let val ths = known ctxt @ facts
in st |>
(assume_tac ctxt ORELSE' resolve_tac ctxt ths THEN_ALL_NEW K no_tac) i
end
else Seq.empty
end)
-(*Simple bidirectional typing tactic, with some nondeterminism from backtracking
- search over input facts. The current implementation does not perform any
- normalization.*)
+(*Simple bidirectional typing tactic with some backtracking search over input
+ facts.*)
fun check_infer_step facts i (ctxt, st) =
let
- val tac = SUBGOAL (fn (goal, i) =>
+ val refine_tac = SUBGOAL (fn (goal, i) =>
if Lib.rigid_typing_concl goal
then
- let val net = Tactic.build_net (
- map (Simplifier.norm_hhf ctxt) facts
- @(cond ctxt)
- @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
- @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
- @(map #1 (Elim.rules ctxt)))
- in (resolve_from_net_tac ctxt net) i end
+ let
+ val net = Tactic.build_net (
+ map (Simplifier.norm_hhf ctxt) facts
+ @(cond ctxt)
+ @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
+ @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
+ @(map #1 (Elim.rules ctxt)))
+ in resolve_from_net_tac ctxt net i end
else no_tac)
+ val sub_tac = 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)
+ andalso Lib.no_vars (Lib.type_of_typing concl)
+ then
+ (resolve_tac ctxt @{thms sub}
+ THEN' SUBGOAL (fn (_, i) =>
+ NO_CONTEXT_TACTIC ctxt (check_infer facts i))
+ THEN' compute_tac ctxt facts
+ THEN_ALL_NEW K no_tac) i
+ else no_tac end)
+
val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
in
- TACTIC_CONTEXT ctxt' (tac i st)
+ TACTIC_CONTEXT ctxt' (
+ (NO_CONTEXT_TACTIC ctxt' o known_ctac facts
+ ORELSE' refine_tac
+ ORELSE' sub_tac) i st)
end
-fun check_infer facts i (cst as (_, st)) =
+and check_infer facts i (cst as (_, st)) =
let
- val ctac = known_ctac facts CORELSE' check_infer_step facts
+ val ctac = 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
+and compute_tac ctxt facts =
+ let
+ val comps = Named_Theorems.get ctxt \<^named_theorems>\<open>comp\<close>
+ val ctxt' = ctxt addsimps comps
+ in
+ SUBGOAL (fn (_, i) =>
+ ((CHANGED o asm_simp_tac ctxt' ORELSE' EqSubst.eqsubst_tac ctxt [0] comps)
+ THEN_ALL_NEW SUBGOAL (fn (_, i) =>
+ NO_CONTEXT_TACTIC ctxt (check_infer facts i))) i)
+ end
+
end
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 13:06:53 +0000