(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.

(REF) Goal statement assumptions are now put into the new context data slots.

(FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data.

(REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context.
  MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`.

(REF) Fixed incompatibilities in theories.

16 files changed, 313 insertions, 178 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 7d1f2b1..a57ed44 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -52,7 +52,7 @@ Lemma (def) hsym:
   shows "g ~ f"
   unfolding homotopy_def
   proof intro
-    fix x assume "x: A" then have "f x = g x"
+    fix x assuming "x: A" then have "f x = g x"
       by (htpy H)
     thus "g x = f x"
       by (rule pathinv) fact
@@ -70,7 +70,7 @@ Lemma (def) htrans:
   shows "f ~ h"
   unfolding homotopy_def
   proof intro
-    fix x assume "x: A"
+    fix x assuming "x: A"
     have *: "f x = g x" "g x = h x"
       by (htpy H1, htpy H2)
     show "f x = h x"
@@ -119,7 +119,7 @@ Lemma funcomp_right_htpy:
   shows "(g \<circ> f) ~ (g \<circ> f')"
   unfolding homotopy_def
   proof (intro, reduce)
-    fix x assume "x: A"
+    fix x assuming "x: A"
     have *: "f x = f' x"
       by (htpy H)
     show "g (f x) = g (f' x)"
@@ -154,18 +154,18 @@ Corollary (def) commute_homotopy':
     "H: f ~ (id A)"
   shows "H (f x) = f [H x]"
   proof -
-    from \<open>H: f ~ id A\<close> have "H: \<Prod>x: A. f x = x"
+    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"
+    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, transport eq: ap_id) (reduce+, refl)
+      by (rule left_whisker, fact *, transport eq: ap_id) (reduce+, 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 *: "{}" by this
+    finally have *: "{}" using * by this
 
     show "H (f x) = f [H x]"
       by pathcomp_cancelr (fact, typechk+)
@@ -179,7 +179,7 @@ subsection \<open>Quasi-inverses\<close>
 definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
   homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"
 
-lemma is_qinv_type [type]:
+Lemma is_qinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_qinv A B f: U i"
   unfolding is_qinv_def
@@ -266,7 +266,7 @@ definition "is_biinv A B f \<equiv>
   (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
     \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
 
-lemma is_biinv_type [type]:
+Lemma is_biinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_biinv A B f: U i"
   unfolding is_biinv_def by typechk
@@ -365,7 +365,7 @@ text \<open>
 definition equivalence (infix "\<simeq>" 110)
   where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
 
-lemma equivalence_type [type]:
+Lemma equivalence_type [type]:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B: U i"
   unfolding equivalence_def by typechk
@@ -432,28 +432,24 @@ Lemma (def) equiv_if_equal:
       \<^enum> vars A B
         apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
         using [[solve_side_conds=1]]
-        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
+        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
         apply (rule transport, rule Ui_in_USi)
-        apply (rule lift_universe_codomain, rule Ui_in_USi)
-        apply (typechk, rule Ui_in_USi)
-        by facts
+        by (rule lift_universe_codomain, rule Ui_in_USi)
       \<^enum> vars A
         using [[solve_side_conds=1]]
         apply (subst transport_comp)
           \<circ> by (rule Ui_in_USi)
           \<circ> by reduce (rule in_USi_if_in_Ui)
-          \<circ> by reduce (rule id_is_biinv, fact)
+          \<circ> by reduce (rule id_is_biinv)
         done
       done
 
     \<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close>
       apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
       using [[solve_side_conds=1]]
-      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
+      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
       apply (rule transport, rule Ui_in_USi)
-      apply (rule lift_universe_codomain, rule Ui_in_USi)
-      apply (typechk, rule Ui_in_USi)
-      by facts
+      by (rule lift_universe_codomain, rule Ui_in_USi)
   done
 
 (*Uncomment this to see all implicits from here on.
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 4829b6f..247d6a4 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -82,7 +82,7 @@ Lemma (def) pathinv:
   shows "y =\<^bsub>A\<^esub> x"
   by (eq p) intro
 
-lemma pathinv_comp [comp]:
+Lemma pathinv_comp [comp]:
   assumes "A: U i" "x: A"
   shows "pathinv A x x (refl x) \<equiv> refl x"
   unfolding pathinv_def by reduce
@@ -94,11 +94,11 @@ Lemma (def) pathcomp:
   shows
     "x =\<^bsub>A\<^esub> z"
   proof (eq p)
-    fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z"
+    fix x q assuming "x: A" and "q: x =\<^bsub>A\<^esub> z"
     show "x =\<^bsub>A\<^esub> z" by (eq q) refl
   qed
 
-lemma pathcomp_comp [comp]:
+Lemma pathcomp_comp [comp]:
   assumes "A: U i" "a: A"
   shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
   unfolding pathcomp_def by reduce
@@ -491,9 +491,9 @@ Lemma (def) right_whisker:
   shows "p \<bullet> r = q \<bullet> r"
   apply (eq r)
     focus vars x s t proof -
-      have "t \<bullet> refl x = t" by (rule pathcomp_refl)
-      also have ".. = s" by fact
-      also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
+      have "s \<bullet> refl x = s" by (rule pathcomp_refl)
+      also have ".. = t" by fact
+      also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric])
       finally show "{}" by this
     qed
   done
@@ -505,9 +505,9 @@ Lemma (def) left_whisker:
   shows "r \<bullet> p = r \<bullet> q"
   apply (eq r)
     focus vars x s t proof -
-      have "refl x \<bullet> t = t" by (rule refl_pathcomp)
-      also have ".. = s" by fact
-      also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric])
+      have "refl x \<bullet> s = s" by (rule refl_pathcomp)
+      also have ".. = t" by fact
+      also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric])
       finally show "{}" by this
     qed
   done
@@ -542,14 +542,13 @@ text \<open>Conditions under which horizontal path-composition is defined.\<clos
 locale horiz_pathcomposable =
 fixes
   i A a b c p q r s
-assumes assums:
+assumes [type]:
   "A: U i" "a: A" "b: A" "c: A"
   "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
   "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
 begin
 
 Lemma (def) horiz_pathcomp:
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
 proof (rule pathcomp)
@@ -560,7 +559,6 @@ qed typechk
 text \<open>A second horizontal composition:\<close>
 
 Lemma (def) horiz_pathcomp':
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
 proof (rule pathcomp)
@@ -572,13 +570,12 @@ notation horiz_pathcomp (infix "\<star>" 121)
 notation horiz_pathcomp' (infix "\<star>''" 121)
 
 Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
   unfolding horiz_pathcomp_def horiz_pathcomp'_def
   apply (eq \<alpha>, eq \<beta>)
     focus vars p apply (eq p)
-      focus vars a q by (eq q) (reduce, refl)
+      focus vars a _ _ _ r by (eq r) (reduce, refl)
     done
   done
 
@@ -597,7 +594,7 @@ Lemma \<Omega>2_alt_def:
 
 section \<open>Eckmann-Hilton\<close>
 
-context fixes i A a assumes "A: U i" "a: A"
+context fixes i A a assumes [type]: "A: U i" "a: A"
 begin
 
 interpretation \<Omega>2:
@@ -619,14 +616,18 @@ 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
-  using assms[unfolded \<Omega>2_alt_def]
+  (*FIXME: Definitional unfolding + normalization; shouldn't need explicit
+    unfolding*)
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof (reduce, rule pathinv)
     \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
-    have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+    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)
     finally have eq\<alpha>: "{} = \<alpha>" by this
 
-    have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+    have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
+      by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
     finally have eq\<beta>: "{} = \<beta>" by this
 
@@ -640,13 +641,15 @@ 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]
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof reduce
-    have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+    have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
+      by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
     finally have eq\<beta>: "{} = \<beta>" by this
 
-    have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+    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)
     finally have eq\<alpha>: "{} = \<alpha>" by this
 
@@ -659,7 +662,7 @@ 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]
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof -
     have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
       by (rule pathcomp_eq_horiz_pathcomp)
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 716703a..f45387c 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -62,17 +62,17 @@ subsection \<open>Addition\<close>
 
 definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n"
 
-lemma add_type [type]:
+Lemma add_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m + n: Nat"
   unfolding add_def by typechk
 
-lemma add_zero [comp]:
+Lemma add_zero [comp]:
   assumes "m: Nat"
   shows "m + 0 \<equiv> m"
   unfolding add_def by reduce
 
-lemma add_suc [comp]:
+Lemma add_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m + suc n \<equiv> suc (m + n)"
   unfolding add_def by reduce
@@ -123,22 +123,22 @@ subsection \<open>Multiplication\<close>
 
 definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n"
 
-lemma mul_type [type]:
+Lemma mul_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m * n: Nat"
   unfolding mul_def by typechk
 
-lemma mul_zero [comp]:
+Lemma mul_zero [comp]:
   assumes "n: Nat"
   shows "n * 0 \<equiv> 0"
   unfolding mul_def by reduce
 
-lemma mul_one [comp]:
+Lemma mul_one [comp]:
   assumes "n: Nat"
   shows "n * 1 \<equiv> n"
   unfolding mul_def by reduce
 
-lemma mul_suc [comp]:
+Lemma mul_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m * suc n \<equiv> m + m * n"
   unfolding mul_def by reduce
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 7f13036..412881b 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -189,7 +189,7 @@ ML_file \<open>context_tactical.ML\<close>
 subsection \<open>Type-checking/inference\<close>
 
 \<comment> \<open>Rule attributes for the type-checker\<close>
-named_theorems form and intr and comp and type
+named_theorems form and intr and comp
 
 \<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
 ML_file \<open>elimination.ML\<close>
@@ -202,7 +202,7 @@ lemmas
   [comp] = beta Sig_comp and
   [cong] = Pi_cong lam_cong Sig_cong
 
-ML_file \<open>typechecking.ML\<close>
+ML_file \<open>types.ML\<close>
 
 method_setup typechk =
   \<open>Scan.succeed (K (CONTEXT_METHOD (
@@ -214,6 +214,7 @@ method_setup known =
 
 subsection \<open>Statement commands\<close>
 
+ML_file \<open>context_facts.ML\<close>
 ML_file \<open>focus.ML\<close>
 ML_file \<open>elaboration.ML\<close>
 ML_file \<open>elaborated_statement.ML\<close>
@@ -374,12 +375,12 @@ translations "f x" \<leftharpoondown> "f `x"
 
 section \<open>Functions\<close>
 
-lemma eta_exp:
+Lemma eta_exp:
   assumes "f: \<Prod>x: A. B x"
   shows "f \<equiv> \<lambda>x: A. f x"
   by (rule eta[symmetric])
 
-lemma refine_codomain:
+Lemma refine_codomain:
   assumes
     "A: U i"
     "f: \<Prod>x: A. B x"
@@ -387,7 +388,7 @@ lemma refine_codomain:
   shows "f: \<Prod>x: A. C x"
   by (subst eta_exp)
 
-lemma lift_universe_codomain:
+Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
   shows "f: A \<rightarrow> U (S j)"
   using in_USi_if_in_Ui[of "f {}"]
@@ -402,7 +403,7 @@ syntax
 translations
   "g \<circ>\<^bsub>A\<^esub> f" \<rightleftharpoons> "CONST funcomp A g f"
 
-lemma funcompI [type]:
+Lemma funcompI [type]:
   assumes
     "A: U i"
     "B: U i"
@@ -413,7 +414,7 @@ lemma funcompI [type]:
     "g \<circ>\<^bsub>A\<^esub> f: \<Prod>x: A. C (f x)"
   unfolding funcomp_def by typechk
 
-lemma funcomp_assoc [comp]:
+Lemma funcomp_assoc [comp]:
   assumes
     "A: U i"
     "f: A \<rightarrow> B"
@@ -423,7 +424,7 @@ lemma funcomp_assoc [comp]:
     "(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 [comp]:
+Lemma funcomp_lambda_comp [comp]:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> b x: B"
@@ -432,7 +433,7 @@ lemma funcomp_lambda_comp [comp]:
     "(\<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 [comp]:
+Lemma funcomp_apply_comp [comp]:
   assumes
     "A: U i" "B: U i" "\<And>x y. x: B \<Longrightarrow> C x: U i"
     "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
@@ -456,12 +457,12 @@ lemma
   id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
   by reduce+
 
-lemma id_left [comp]:
+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)
 
-lemma id_right [comp]:
+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)
@@ -476,23 +477,23 @@ section \<open>Pairs\<close>
 definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn _. A) (fn x y. x) p"
 definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p"
 
-lemma fst_type [type]:
+Lemma fst_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
   shows "fst A B: (\<Sum>x: A. B x) \<rightarrow> A"
   unfolding fst_def by typechk
 
-lemma fst_comp [comp]:
+Lemma fst_comp [comp]:
   assumes
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
   shows "fst A B <a, b> \<equiv> a"
   unfolding fst_def by reduce
 
-lemma snd_type [type]:
+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
 
-lemma snd_comp [comp]:
+Lemma snd_comp [comp]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
   shows "snd A B <a, b> \<equiv> b"
   unfolding snd_def by reduce
diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML
new file mode 100644
index 0000000..4b4bcd9
--- /dev/null
+++ b/spartan/core/context_facts.ML
@@ -0,0 +1,44 @@
+structure Context_Facts: sig
+
+val Eq: Proof.context -> thm Item_Net.T
+val eq: Proof.context -> thm list
+val eq_of: Proof.context -> term -> thm list
+val register_eq: thm -> Context.generic -> Context.generic
+val register_eqs: thm list -> Context.generic -> Context.generic
+val register_facts: thm list -> Proof.context -> Proof.context
+
+end = struct
+
+
+(* Equality statements *)
+
+structure Eq = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o (#1 o Lib.dest_eq) o Thm.concl_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+val Eq = Eq.get o Context.Proof
+val eq = Item_Net.content o Eq
+fun eq_of ctxt tm = Item_Net.retrieve (Eq ctxt) tm
+
+fun register_eq rule =
+  if Lib.is_eq (Thm.concl_of rule) then Eq.map (Item_Net.update rule)
+  else error "Not a definitional equality judgment"
+
+fun register_eqs rules = foldr1 (op o) (map register_eq rules)
+
+
+(* Context assumptions *)
+
+fun register_facts ths =
+  let
+    val (facts, conds, eqs) = Lib.partition_judgments ths
+    val f = Types.register_knowns facts handle Empty => I
+    val c = Types.register_conds conds handle Empty => I
+    val e = register_eqs eqs handle Empty => I
+  in Context.proof_map (e o c o f) end
+
+end
diff --git a/spartan/core/elaborated_statement.ML b/spartan/core/elaborated_statement.ML
index 81f4a7d..33f88cf 100644
--- a/spartan/core/elaborated_statement.ML
+++ b/spartan/core/elaborated_statement.ML
@@ -416,6 +416,35 @@ val structured_statement =
   Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
     >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows))
 
+fun these_factss more_facts (named_factss, state) =
+  (named_factss, state |> Proof.set_facts (maps snd named_factss @ more_facts))
+
+fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
+  let
+    val ctxt = Proof.context_of state;
+
+    val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
+    val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} =
+      #1 (prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt);
+    val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
+  in
+    state
+    |> Proof.assert_forward
+    |> Proof.map_context_result (fn ctxt =>
+      ctxt
+      |> Proof_Context.augment text
+      |> fold Variable.maybe_bind_term result_binds
+      |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
+      |-> (fn premss => fn ctxt =>
+            (premss, Context_Facts.register_facts (flat premss) ctxt))
+      |-> (fn premss =>
+        Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss)))
+    |> these_factss [] |> #2
+  end
+
+val assume =
+  gen_assume Proof_Context.cert_statement (K I) Assumption.assume_export
+
 in
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elaborated assumption"
@@ -433,7 +462,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elabora
       val c' = c |> map (fn ((b, atts), ss) =>
         ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss))
       val c'' = Elab.elaborate ctxt [] c'
-    in Proof.assume a' b' c'' state end)))
+    in assume a' b' c'' state end)))
 
 end
 
diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML
index cd4e414..cf9d21e 100644
--- a/spartan/core/elimination.ML
+++ b/spartan/core/elimination.ML
@@ -41,7 +41,7 @@ val _ = Theory.setup (
       (Thm.declaration_attribute o register_rule))
     ""
   #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elim\<close>,
-      fn context => (map #1 (rules (Context.proof_of context))))
+      fn context => map #1 (rules (Context.proof_of context)))
 )
 
 
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML
index 2ad4c8a..b963cfe 100644
--- a/spartan/core/focus.ML
+++ b/spartan/core/focus.ML
@@ -117,7 +117,8 @@ fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state =
     |> Proof.map_context (fn _ =>
       #context subgoal_focus
       |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])]
-      |> #2)
+      |> snd
+      |> Context_Facts.register_facts prems)
     |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
         NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])]
     |> #2
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index a04bd0e..7d52495 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -175,7 +175,8 @@ fun gen_schematic_theorem
   in
     goal_ctxt
     |> not (null prems) ?
-      (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
+      (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])]
+        #> snd #> Context_Facts.register_facts prems)
     |> Proof.theorem before_qed gen_and_after_qed (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
   end
@@ -188,12 +189,12 @@ val schematic_theorem_cmd =
 
 fun theorem spec descr =
   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
-    ( Scan.option (Args.parens (Args.$$$ "def"))
+    (Scan.option (Args.parens (Args.$$$ "def"))
       -- (long_statement || short_statement) >>
         (fn (opt_derive, (long, binding, includes, elems, concl)) =>
           schematic_theorem_cmd
             (case opt_derive of SOME "def" => true | _ => false)
-            long descr NONE (K I) binding includes elems concl) )
+            long descr NONE (K I) binding includes elems concl))
 
 fun definition spec descr =
   Outer_Syntax.local_theory_to_proof' spec "definition via proof"
diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML
index 392ae2e..e43ad98 100644
--- a/spartan/core/lib.ML
+++ b/spartan/core/lib.ML
@@ -27,6 +27,9 @@ val typing_of_term: term -> term
 val decompose_goal: Proof.context -> term -> term list * term
 val rigid_typing_concl: term -> bool
 
+(*Theorems*)
+val partition_judgments: thm list -> thm list * thm list * thm list
+
 (*Subterms*)
 val has_subterm: term list -> term -> bool
 val subterm_count: term -> term -> int
@@ -121,6 +124,19 @@ fun rigid_typing_concl goal =
   in is_typing concl andalso is_rigid (term_of_typing concl) end
 
 
+(** Theorems **)
+fun partition_judgments ths =
+  let
+    fun part [] facts conds eqs = (facts, conds, eqs)
+      | part (th::ths) facts conds eqs =
+          if is_typing (Thm.prop_of th) then
+            part ths (th::facts) conds eqs
+          else if is_typing (Thm.concl_of th) then
+            part ths facts (th::conds) eqs
+          else part ths facts conds (th::eqs)
+  in part ths [] [] [] end
+
+
 (** Subterms **)
 
 fun has_subterm tms =
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 45fd119..0c46ef0 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -82,8 +82,8 @@ fun internalize_fact_tac t =
         Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
     in
       HEADGOAL (resolve_tac ctxt [resolvent])
-      (*Infer the correct type T*)
-      THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.check_infer [])
+      (*Unify with the correct type T*)
+      THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac [])
     end)
 
 fun elim_core_tac tms types ctxt =
@@ -111,18 +111,16 @@ fun elim_ctac tms =
     [] => 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 facts = map Thm.prop_of (Types.known 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
+        val types = filter (fn th => Term.could_unify (template, th)) (facts @ 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
+              val inserts = facts @ prems
                 |> filter Lib.is_typing
                 |> map Lib.dest_typing
                 |> filter_out (fn (t, _) =>
@@ -170,7 +168,7 @@ fun cases_ctac tm =
           | [] => 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))
+            error ("No case rule known for " ^ (Syntax.string_of_term ctxt tm))
       in
         resolve_tac ctxt [res] i
       end)
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
deleted file mode 100644
index ca89c8c..0000000
--- a/spartan/core/typechecking.ML
+++ /dev/null
@@ -1,96 +0,0 @@
-(*  Title:      typechecking.ML
-    Author:     Joshua Chen
-
-Type information and type-checking infrastructure.
-*)
-
-structure Types: sig
-
-val Data: Proof.context -> thm Item_Net.T
-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 debug_typechk: bool Config.T
-
-val known_ctac: thm list -> int -> context_tactic
-val check_infer: thm list -> int -> context_tactic
-
-end = struct
-
-
-(* Context data *)
-
-structure Data = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o Lib.term_of_typing o Thm.prop_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Data = Data.get o Context.Proof
-fun types ctxt tm = Item_Net.retrieve (Data ctxt) tm
-fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
-fun put_types typings = foldr1 (op o) (map put_type typings)
-
-
-(* Context tactics for type-checking *)
-
-val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
-
-fun debug_tac ctxt s =
-  if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
-
-(*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 = map (Simplifier.norm_hhf 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 arbitrary `type` rules. The current implementation does not
-  perform any normalization.*)
-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 (
-          map (Simplifier.norm_hhf ctxt)
-            (*FIXME: Shouldn't pull nameless facts directly from context. Note
-              that we *do* need to be able to resolve with conditional
-              statements expressing type family judgments*)
-            (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
-          (*MAYBE FIXME: Remove `type` from this list, and instead perform
-            definitional unfolding to (w?)hnf.*)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>)
-          @(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 ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
-  in
-    TACTIC_CONTEXT ctxt' (tac i st)
-  end
-
-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
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
new file mode 100644
index 0000000..a521f7c
--- /dev/null
+++ b/spartan/core/types.ML
@@ -0,0 +1,141 @@
+(*  Title:      typechecking.ML
+    Author:     Joshua Chen
+
+Type information and type-checking infrastructure.
+*)
+
+structure Types: sig
+
+val Known: Proof.context -> thm Item_Net.T
+val known: Proof.context -> thm list
+val known_of: Proof.context -> term -> thm list
+val register_known: thm -> Context.generic -> Context.generic
+val register_knowns: thm list -> Context.generic -> Context.generic
+
+val Cond: Proof.context -> thm Item_Net.T
+val cond: Proof.context -> thm list
+val cond_of: Proof.context -> term -> thm list
+val register_cond: thm -> Context.generic -> Context.generic
+val register_conds: thm list -> Context.generic -> Context.generic
+
+val debug_typechk: bool Config.T
+
+val known_ctac: thm list -> int -> context_tactic
+val check_infer: thm list -> int -> context_tactic
+
+end = struct
+
+
+(** Context data **)
+
+(* Known types *)
+
+structure Known = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o Lib.term_of_typing o Thm.prop_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+val Known = Known.get o Context.Proof
+val known = Item_Net.content o Known
+fun known_of ctxt tm = Item_Net.retrieve (Known ctxt) tm
+
+fun register_known typing =
+  if Lib.is_typing (Thm.prop_of typing) then Known.map (Item_Net.update typing)
+  else error "Not a type judgment"
+
+fun register_knowns typings = foldr1 (op o) (map register_known typings)
+
+(* Conditional type rules *)
+
+(*Two important cases: 1. general type inference rules and 2. type family
+  judgments*)
+
+structure Cond = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o Lib.term_of_typing o Thm.concl_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+val Cond = Cond.get o Context.Proof
+val cond = Item_Net.content o Cond
+fun cond_of ctxt tm = Item_Net.retrieve (Cond ctxt) tm
+
+fun register_cond rule =
+  if Lib.is_typing (Thm.concl_of rule) then Cond.map (Item_Net.update rule)
+  else error "Not a conditional type judgment"
+
+fun register_conds rules = foldr1 (op o) (map register_cond rules)
+
+
+(** [type] attribute **)
+
+val _ = Theory.setup (
+  Attrib.setup \<^binding>\<open>type\<close>
+    (Scan.succeed (Thm.declaration_attribute (fn th =>
+      if Thm.no_prems th then register_known th else register_cond th)))
+    ""
+  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>type\<close>,
+      fn context => let val ctxt = Context.proof_of context in
+        known ctxt @ cond ctxt end)
+)
+
+
+(** Context tactics for type-checking and elaboration **)
+
+val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
+
+fun debug_tac ctxt s =
+  if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
+
+(*Solves goals without metavariables and type inference problems by assumption
+  from inline premises or resolution with facts*)
+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 = known ctxt @ map (Simplifier.norm_hhf 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.*)
+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 (
+          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 ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
+  in
+    TACTIC_CONTEXT ctxt' (tac i st)
+  end
+
+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
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index dd51582..83e5149 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -149,7 +149,7 @@ Definition map:
 proof (elim xs)
   show "[]: List B" by intro
   next fix x ys
-    assume "x: A" "ys: List B"
+  assuming "x: A" "ys: List B"
   show "f x # ys: List B" by typechk
 qed
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 0a7ec21..da22a4e 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -25,10 +25,10 @@ Definition MaybeInd:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
   shows "C m"
-  using assms[unfolded Maybe_def none_def some_def]
+  using assms[unfolded Maybe_def none_def some_def, type]
   apply (elim m)
-    apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
-    apply (elim, rule \<open>_: C (inr _ _ _)\<close>)
+    apply fact
+    apply (elim, fact)
   done
 
 Lemma Maybe_comp_none:
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 6adbce8..c0abf31 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -105,7 +105,8 @@ Definition ifelse [rotated 1]:
     "a: C true"
     "b: C false"
   shows "C x"
-  by (elim x) (elim, rule *)+
+  using assms[unfolded Bool_def true_def false_def, type]
+  by (elim x) (elim, fact)+
 
 Lemma if_true:
   assumes