(FEAT) Term elaboration of assumption and goal statements.

  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.

17 files changed, 670 insertions, 528 deletions

diff --git a/ROOT b/ROOT
index 00d020a..b3aa520 100644
--- a/ROOT
+++ b/ROOT
@@ -14,7 +14,7 @@ session Spartan in spartan = Spartan_Core +
   directories
     lib
   theories
-    More_Types
+    Prelude
     Maybe
     List
 
@@ -29,6 +29,4 @@ session HoTT in hott = Spartan +
     Identity
     Equivalence
     Nat
-    More_List
-    More_Nat
-
+    "List+"
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index d844b59..66c64f6 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -16,53 +16,68 @@ Lemma homotopy_type [typechk]:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> B x: U i"
-    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+    "f: \<Prod>x: A. B x"
+    "g: \<Prod>x: A. B x"
   shows "f ~ g: U i"
-  unfolding homotopy_def by typechk
+  unfolding homotopy_def
+  by typechk
 
-Lemma (derive) homotopy_refl [refl]:
+Lemma apply_homotopy:
+  assumes
+    "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+    "H: f ~ g"
+    "x: A"
+  shows "H x: f x = g x"
+  using \<open>H:_\<close> unfolding homotopy_def
+  by typechk
+
+method htpy for H::o = rule apply_homotopy[where ?H=H]
+
+Lemma (def) homotopy_refl [refl]:
   assumes
     "A: U i"
     "f: \<Prod>x: A. B x"
   shows "f ~ f"
-  unfolding homotopy_def by intros
+  unfolding homotopy_def
+  by intros
 
-Lemma (derive) hsym:
+Lemma (def) hsym:
   assumes
-    "f: \<Prod>x: A. B x"
-    "g: \<Prod>x: A. B x"
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> B x: U i"
+    "f: \<Prod>x: A. B x"
+    "g: \<Prod>x: A. B x"
     "H: f ~ g"
   shows "g ~ f"
-unfolding homotopy_def
-proof intro
-  fix x assume "x: A" then have "H x: f x = g x"
-    using \<open>H:_\<close>[unfolded homotopy_def]
-      \<comment> \<open>this should become unnecessary when definitional unfolding is implemented\<close>
-    by typechk
-  thus "g x = f x" by (rule pathinv) fact
-qed typechk
-
-Lemma (derive) htrans:
+  unfolding homotopy_def
+  proof intro
+    fix x assume "x: A" then have "f x = g x"
+      by (htpy H)
+    thus "g x = f x"
+      by (rule pathinv) fact
+  qed
+
+Lemma (def) htrans:
   assumes
+    "A: U i"
+    "\<And>x. x: A \<Longrightarrow> B x: U i"
     "f: \<Prod>x: A. B x"
     "g: \<Prod>x: A. B x"
     "h: \<Prod>x: A. B x"
-    "A: U i"
-    "\<And>x. x: A \<Longrightarrow> B x: U i"
-  shows "\<lbrakk>H1: f ~ g; H2: g ~ h\<rbrakk> \<Longrightarrow> f ~ h"
+    "H1: f ~ g"
+    "H2: g ~ h"
+  shows "f ~ h"
   unfolding homotopy_def
-  apply intro
-    \<guillemotright> vars x
-      apply (rule pathcomp[where ?y="g x"])
-        \<^item> by (elim H1)
-        \<^item> by (elim H2)
-      done
-    \<guillemotright> by typechk
-  done
+  proof intro
+    fix x assume "x: A"
+    have *: "f x = g x" "g x = h x"
+      by (htpy H1, htpy H2)
+    show "f x = h x"
+      by (rule pathcomp; (rule *)?) typechk
+  qed
 
-text \<open>For calculations:\<close>
+section \<open>Rewriting homotopies\<close>
 
 congruence "f ~ g" rhs g
 
@@ -70,229 +85,258 @@ lemmas
   homotopy_sym [sym] = hsym[rotated 4] and
   homotopy_trans [trans] = htrans[rotated 5]
 
-Lemma (derive) commute_homotopy:
-  assumes
-    "A: U i" "B: U i"
-    "x: A" "y: A"
-    "p: x = y"
-    "f: A \<rightarrow> B" "g: A \<rightarrow> B"
-    "H: f ~ g"
-  shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
-  \<comment> \<open>Need this assumption unfolded for typechecking\<close>
-  supply assms(8)[unfolded homotopy_def]
-  apply (eq p)
-    focus vars x
-      apply reduce
-        \<comment> \<open>Here it would really be nice to have automation for transport and
-          propositional equality.\<close>
-        apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"])
-          \<guillemotright> by (rule pathcomp_refl)
-          \<guillemotright> by (rule pathinv) (rule refl_pathcomp)
-          \<guillemotright> by typechk
-    done
-  done
-
-Corollary (derive) commute_homotopy':
-  assumes
-    "A: U i"
-    "x: A"
-    "f: A \<rightarrow> A"
-    "H: f ~ (id A)"
-  shows "H (f x) = f [H x]"
-oops
-
-Lemma homotopy_id_left [typechk]:
+Lemma id_funcomp_htpy:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "homotopy_refl A f: (id B) \<circ> f ~ f"
-  unfolding homotopy_refl_def homotopy_def by reduce
+  by reduce
 
-Lemma homotopy_id_right [typechk]:
+Lemma funcomp_id_htpy:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "homotopy_refl A f: f \<circ> (id A) ~ f"
-  unfolding homotopy_refl_def homotopy_def
- by reduce
+  by reduce
 
-Lemma homotopy_funcomp_left:
+Lemma funcomp_left_htpy:
   assumes
-    "H: homotopy B C g g'"
+    "A: U i" "B: U i"
+    "\<And>x. x: B \<Longrightarrow> C x: U i"
     "f: A \<rightarrow> B"
     "g: \<Prod>x: B. C x"
     "g': \<Prod>x: B. C x"
-    "A: U i" "B: U i"
-    "\<And>x. x: B \<Longrightarrow> C x: U i"
-  shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g' \<circ>\<^bsub>A\<^esub> f)"
+    "H: g ~ g'"
+  shows "(g \<circ> f) ~ (g' \<circ> f)"
   unfolding homotopy_def
-  apply (intro; reduce)
-    apply (insert \<open>H: _\<close>[unfolded homotopy_def])
-      apply (elim H)
+  apply (intro, reduce)
+  apply (htpy H)
   done
 
-Lemma homotopy_funcomp_right:
+Lemma funcomp_right_htpy:
   assumes
-    "H: homotopy A (fn _. B) f f'"
+    "A: U i" "B: U i" "C: U i"
     "f: A \<rightarrow> B"
     "f': A \<rightarrow> B"
     "g: B \<rightarrow> C"
-    "A: U i" "B: U i" "C: U i"
-  shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g \<circ>\<^bsub>A\<^esub> f')"
+    "H: f ~ f'"
+  shows "(g \<circ> f) ~ (g \<circ> f')"
   unfolding homotopy_def
-  apply (intro; reduce)
-    apply (insert \<open>H: _\<close>[unfolded homotopy_def])
-      apply (dest PiE, assumption)
-      apply (rule ap, assumption)
-  done
+  proof (intro, reduce)
+    fix x assume "x: A"
+    have *: "f x = f' x"
+      by (htpy H)
+    show "g (f x) = g (f' x)"
+      by (transport eq: *) refl
+  qed
 
-method id_htpy = (rule homotopy_id_left)
-method htpy_id = (rule homotopy_id_right)
-method htpy_o = (rule homotopy_funcomp_left)
-method o_htpy = (rule homotopy_funcomp_right)
+method lhtpy = rule funcomp_left_htpy[rotated 6]
+method rhtpy = rule funcomp_right_htpy[rotated 6]
+
+
+Lemma (def) commute_homotopy:
+  assumes
+    "A: U i" "B: U i"
+    "x: A" "y: A"
+    "p: x = y"
+    "f: A \<rightarrow> B" "g: A \<rightarrow> B"
+    "H: f ~ g"
+  shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
+  using \<open>H:_\<close>
+  unfolding homotopy_def
+  apply (eq p, reduce)
+  apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp)
+  by refl
+
+Corollary (def) commute_homotopy':
+  assumes
+    "A: U i"
+    "x: A"
+    "f: A \<rightarrow> A"
+    "H: f ~ (id A)"
+  shows "H (f x) = f [H x]"
+oops
 
 
 section \<open>Quasi-inverse and bi-invertibility\<close>
 
 subsection \<open>Quasi-inverses\<close>
 
-definition "qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
+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 qinv_type [typechk]:
+lemma is_qinv_type [typechk]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "qinv A B f: U i"
-  unfolding qinv_def by typechk
+  shows "is_qinv A B f: U i"
+  unfolding is_qinv_def
+  by typechk
 
-definition qinv_i ("qinv")
-  where [implicit]: "qinv f \<equiv> Equivalence.qinv ? ? f"
+definition is_qinv_i ("is'_qinv")
+  where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv ? ? f"
 
-translations "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"
+no_translations "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f"
 
-Lemma (derive) id_qinv:
+Lemma (def) id_is_qinv:
   assumes "A: U i"
-  shows "qinv (id A)"
-  unfolding qinv_def
+  shows "is_qinv (id A)"
+  unfolding is_qinv_def
   proof intro
     show "id A: A \<rightarrow> A" by typechk
   qed (reduce, intro; refl)
 
-Lemma (derive) quasiinv_qinv:
-  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "prf: qinv f \<Longrightarrow> qinv (fst prf)"
-  unfolding qinv_def
-  apply intro
-  \<guillemotright> by (rule \<open>f:_\<close>)
-  \<guillemotright> apply (elim "prf")
-    focus vars g HH
-      apply intro
-        \<^item> by reduce (snd HH)
-        \<^item> by reduce (fst HH)
-    done
-    done
+Lemma is_qinvI:
+  assumes
+    "A: U i" "B: U i" "f: A \<rightarrow> B"
+    "g: B \<rightarrow> A"
+    "H1: g \<circ> f ~ id A"
+    "H2: f \<circ> g ~ id B"
+  shows "is_qinv f"
+  unfolding is_qinv_def
+  proof intro
+    show "g: B \<rightarrow> A" by fact
+    show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact)
+  qed
+
+Lemma is_qinv_components [typechk]:
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
+  shows
+    fst_of_is_qinv: "fst pf: B \<rightarrow> A" and
+    p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
+    p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
+  using assms unfolding is_qinv_def
+  by typechk+
+
+Lemma (def) qinv_is_qinv:
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
+  shows "is_qinv (fst pf)"
+using [[debug_typechk]]
+  using [[solve_side_conds=2]]
+  apply (rule is_qinvI)
+  back \<comment> \<open>Typechecking/inference goes too far here. Problem would likely be
+    solved with definitional unfolding\<close>
+  \<^item> by (fact \<open>f:_\<close>)
+  \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv)
+  \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv)
   done
 
-Lemma (derive) funcomp_qinv:
+Lemma (def) funcomp_is_qinv:
   assumes
     "A: U i" "B: U i" "C: U i"
     "f: A \<rightarrow> B" "g: B \<rightarrow> C"
-  shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
-  apply (intros, unfold qinv_def, elims)
-  focus prems vars _ _ finv _ ginv
-    apply (intro, rule funcompI[where ?f=ginv and ?g=finv])
-    proof (reduce, intro)
-      have "finv \<circ> ginv \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
-      also have ".. ~ finv \<circ> id B \<circ> f" by (o_htpy, htpy_o) fact
-      also have ".. ~ id A" by reduce fact
-      finally show "finv \<circ> ginv \<circ> g \<circ> f ~ id A" by this
-
-      have "g \<circ> f \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
-      also have ".. ~ g \<circ> id B \<circ> ginv" by (o_htpy, htpy_o) fact
-      also have ".. ~ id C" by reduce fact
-      finally show "g \<circ> f \<circ> finv \<circ> ginv ~ id C" by this
-    qed
+  shows "is_qinv f \<rightarrow> is_qinv g \<rightarrow> is_qinv (g \<circ> f)"
+  apply intros
+  unfolding is_qinv_def apply elims
+  focus vars _ _ finv _ ginv
+    apply intro
+    \<^item> by (rule funcompI[where ?f=ginv and ?g=finv])
+    \<^item> proof intro
+        show "(finv \<circ> ginv) \<circ> g \<circ> f ~ id A"
+        proof -
+          have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
+          also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact
+          also have ".. ~ id A" by reduce fact
+          finally show "{}" by this
+        qed
+    
+        show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C"
+        proof -
+          have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
+          also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact
+          also have ".. ~ id C" by reduce fact
+          finally show "{}" by this
+        qed
+      qed
+    done
   done
 
 subsection \<open>Bi-invertible maps\<close>
 
-definition "biinv A B f \<equiv>
+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 biinv_type [typechk]:
+lemma is_biinv_type [typechk]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "biinv A B f: U i"
-  unfolding biinv_def by typechk
+  shows "is_biinv A B f: U i"
+  unfolding is_biinv_def by typechk
 
-definition biinv_i ("biinv")
-  where [implicit]: "biinv f \<equiv> Equivalence.biinv ? ? f"
+definition is_biinv_i ("is'_biinv")
+  where [implicit]: "is_biinv f \<equiv> Equivalence.is_biinv ? ? f"
 
-translations "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"
+translations "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f"
 
-Lemma (derive) qinv_imp_biinv:
+Lemma is_biinvI:
   assumes
-    "A: U i" "B: U i"
-    "f: A \<rightarrow> B"
-  shows "?prf: qinv f \<rightarrow> biinv f"
-  apply intros
-  unfolding qinv_def biinv_def
-  by (rule Sig_dist_exp)
-
-text \<open>
-  Show that bi-invertible maps are quasi-inverses, as a demonstration of how to
-  work in this system.
-\<close>
+    "A: U i" "B: U i" "f: A \<rightarrow> B"
+    "g: B \<rightarrow> A" "h: B \<rightarrow> A"
+    "H1: g \<circ> f ~ id A" "H2: f \<circ> h ~ id B"
+  shows "is_biinv f"
+  unfolding is_biinv_def
+  proof intro
+    show "<g, H1>: {}" by typechk
+    show "<h, H2>: {}" by typechk
+  qed
 
-Lemma (derive) biinv_imp_qinv:
+Lemma is_biinv_components [typechk]:
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f"
+  shows
+    p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
+    p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
+    p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
+    p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
+  using assms unfolding is_biinv_def
+  by typechk+
+
+Lemma (def) is_qinv_imp_is_biinv:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
-  shows "biinv f \<rightarrow> qinv f"
+  shows "is_qinv f \<rightarrow> is_biinv f"
+  apply intros
+  unfolding is_qinv_def is_biinv_def
+  by (rule distribute_Sig)
 
-  text \<open>Split the hypothesis \<^term>\<open>biinv f\<close> into its components:\<close>
-  apply intro
-  unfolding biinv_def
-  apply elims
-
-  text \<open>Name the components:\<close>
-  focus prems vars _ _ _ g H1 h H2
-  thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close>
-
-  text \<open>
-    \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>, so the proof will be a triple
-    \<^term>\<open><g, <?H1, ?H2>>\<close>.
-  \<close>
-  unfolding qinv_def
+Lemma (def) is_biinv_imp_is_qinv:
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+  shows "is_biinv f \<rightarrow> is_qinv f"
   apply intro
-    \<guillemotright> by (fact \<open>g: _\<close>)
-    \<guillemotright> apply intro
-      text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close>
-      apply (fact \<open>H1: _\<close>)
 
+  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 to calculate "forward".
+        block is used for calculational reasoning.
       \<close>
-      proof -
-        have "g ~ g \<circ> (id B)" by reduce refl
-        also have ".. ~ g \<circ> f \<circ> h" by o_htpy (rule \<open>H2:_\<close>[symmetric])
-        also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact)
-        also have ".. ~ h" by reduce refl
-        finally have "g ~ h" by this
-        then have "f \<circ> g ~ f \<circ> h" by (o_htpy, this)
-        also note \<open>H2:_\<close>
-        finally show "f \<circ> g ~ id B" by this
-      qed
+      \<^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])
+          also have ".. ~ (id A) \<circ> h" by (rewrite funcomp_assoc[symmetric]) (lhtpy, fact)
+          also have ".. ~ h" by reduce refl
+          finally have "g ~ h" by this
+          then have "f \<circ> g ~ f \<circ> h" by (rhtpy, this)
+          also note \<open>H2:_\<close>
+          finally show "f \<circ> g ~ id B" by this
+        qed
     done
   done
 
-Lemma (derive) id_biinv:
-  "A: U i \<Longrightarrow> biinv (id A)"
-  by (rule qinv_imp_biinv) (rule id_qinv)
+Lemma (def) id_is_biinv:
+  "A: U i \<Longrightarrow> is_biinv (id A)"
+  by (rule is_qinv_imp_is_biinv) (rule id_is_qinv)
 
-Lemma (derive) funcomp_biinv:
+Lemma (def) funcomp_is_biinv:
   assumes
     "A: U i" "B: U i" "C: U i"
     "f: A \<rightarrow> B" "g: B \<rightarrow> C"
-  shows "biinv f \<rightarrow> biinv g \<rightarrow> biinv (g \<circ> f)"
+  shows "is_biinv f \<rightarrow> is_biinv g \<rightarrow> is_biinv (g \<circ> f)"
   apply intros
-  focus vars biinv\<^sub>f biinv\<^sub>g
-    by (rule qinv_imp_biinv) (rule funcomp_qinv; rule biinv_imp_qinv)
+  focus vars pf pg
+    by (rule is_qinv_imp_is_biinv)
+       (rule funcomp_is_qinv; rule is_biinv_imp_is_qinv, fact)
   done
 
 
@@ -304,19 +348,19 @@ text \<open>
 \<close>
 
 definition equivalence (infix "\<simeq>" 110)
-  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.biinv A B f"
+  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
 
 lemma equivalence_type [typechk]:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B: U i"
   unfolding equivalence_def by typechk
 
-Lemma (derive) equivalence_refl:
+Lemma (def) equivalence_refl:
   assumes "A: U i"
   shows "A \<simeq> A"
   unfolding equivalence_def
   proof intro
-    show "biinv (id A)" by (rule qinv_imp_biinv) (rule id_qinv)
+    show "is_biinv (id A)" by (rule is_qinv_imp_is_biinv) (rule id_is_qinv)
   qed typechk
 
 text \<open>
@@ -324,32 +368,30 @@ text \<open>
   univalence?)...
 \<close>
 
-Lemma (derive) equivalence_symmetric:
+Lemma (def) equivalence_symmetric:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B \<rightarrow> B \<simeq> A"
   apply intros
   unfolding equivalence_def
   apply elim
-  \<guillemotright> vars _ f "prf"
-    apply (dest (4) biinv_imp_qinv)
-    apply intro
-      \<^item> unfolding qinv_def by (rule fst[of "(biinv_imp_qinv A B f) prf"])
-      \<^item> by (rule qinv_imp_biinv) (rule quasiinv_qinv)
-    done
+  apply (dest (4) is_biinv_imp_is_qinv)
+  apply intro
+    \<^item> by (rule fst_of_is_qinv) facts
+    \<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv)
   done
 
-Lemma (derive) equivalence_transitive:
+Lemma (def) equivalence_transitive:
   assumes "A: U i" "B: U i" "C: U i"
   shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
   proof intros
     fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C"
     then have
-      "fst AB: A \<rightarrow> B" and 1: "snd AB: biinv (fst AB)"
-      "fst BC: B \<rightarrow> C" and 2: "snd BC: biinv (fst BC)"
+      "fst AB: A \<rightarrow> B" and 1: "snd AB: is_biinv (fst AB)"
+      "fst BC: B \<rightarrow> C" and 2: "snd BC: is_biinv (fst BC)"
       unfolding equivalence_def by typechk+
     then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk
-    moreover have "biinv (fst BC \<circ> fst AB)"
-      using * unfolding equivalence_def by (rules funcomp_biinv 1 2)
+    moreover have "is_biinv (fst BC \<circ> fst AB)"
+      using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts
     ultimately show "A \<simeq> C"
       unfolding equivalence_def by intro facts
   qed
@@ -370,14 +412,14 @@ text \<open>
   (2) we don't yet have universe automation.
 \<close>
 
-Lemma (derive) id_imp_equiv:
+Lemma (def) id_imp_equiv:
   assumes
     "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
   shows "<trans (id (U i)) p, ?isequiv>: A \<simeq> B"
   unfolding equivalence_def
   apply intros defer
-    \<guillemotright> apply (eq p)
-      \<^item> prems vars A B
+    \<^item> apply (eq p)
+      \<^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])
@@ -385,16 +427,16 @@ Lemma (derive) id_imp_equiv:
         apply (rule lift_universe_codomain, rule Ui_in_USi)
         apply (typechk, rule Ui_in_USi)
         done
-      \<^item> prems vars A
+      \<^enum> vars A
         using [[solve_side_conds=1]]
         apply (subst transport_comp)
-          \<^enum> by (rule Ui_in_USi)
-          \<^enum> by reduce (rule in_USi_if_in_Ui)
-          \<^enum> by reduce (rule id_biinv)
+          \<circ> by (rule Ui_in_USi)
+          \<circ> by reduce (rule in_USi_if_in_Ui)
+          \<circ> by reduce (rule id_is_biinv)
         done
       done
 
-    \<guillemotright> \<comment> \<open>Similar proof as in the first subgoal above\<close>
+    \<^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])
@@ -419,8 +461,8 @@ no_translations
   "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"
-  "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"
-  "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"
+  "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f"
+  "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f"
 *)
 
 
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 728537c..d6efbf8 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -42,7 +42,7 @@ axiomatization where
 lemmas
   [form] = IdF and
   [intro, intros] = IdI and
-  [elim "?p" "?a" "?b"] = IdE and
+  [elim ?p ?a ?b] = IdE and
   [comp] = Id_comp and
   [refl] = IdI
 
@@ -77,34 +77,34 @@ method_setup eq =
 
 section \<open>Symmetry and transitivity\<close>
 
-Lemma (derive) pathinv:
+Lemma (def) pathinv:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
   shows "y =\<^bsub>A\<^esub> x"
   by (eq p) intro
 
 lemma pathinv_comp [comp]:
-  assumes "x: A" "A: U i"
+  assumes "A: U i" "x: A"
   shows "pathinv A x x (refl x) \<equiv> refl x"
   unfolding pathinv_def by reduce
 
-Lemma (derive) pathcomp:
+Lemma (def) pathcomp:
   assumes
     "A: U i" "x: A" "y: A" "z: A"
     "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z"
   shows
     "x =\<^bsub>A\<^esub> z"
-  apply (eq p)
-    focus prems vars x p
-      apply (eq p)
-        apply intro
-    done
-  done
+  proof (eq p)
+    fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z"
+    show "x =\<^bsub>A\<^esub> z" by (eq q) refl
+  qed
 
 lemma pathcomp_comp [comp]:
-  assumes "a: A" "A: U i"
+  assumes "A: U i" "a: A"
   shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
   unfolding pathcomp_def by reduce
 
+method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
+
 
 section \<open>Notation\<close>
 
@@ -134,26 +134,22 @@ lemmas
 
 section \<open>Basic propositional equalities\<close>
 
-Lemma (derive) refl_pathcomp:
+Lemma (def) refl_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "(refl x) \<bullet> p = p"
-  apply (eq p)
-    apply (reduce; intro)
-  done
+  by (eq p) (reduce, refl)
 
-Lemma (derive) pathcomp_refl:
+Lemma (def) pathcomp_refl:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p \<bullet> (refl y) = p"
-  apply (eq p)
-    apply (reduce; intro)
-  done
+  by (eq p) (reduce, refl)
 
-definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p"
 definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p"
+definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p"
 
 translations
-  "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p"
   "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p"
+  "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p"
 
 Lemma lu_refl [comp]:
   assumes "A: U i" "x: A"
@@ -165,40 +161,40 @@ Lemma ru_refl [comp]:
   shows "ru (refl x) \<equiv> refl (refl x)"
   unfolding pathcomp_refl_def by reduce
 
-Lemma (derive) inv_pathcomp:
+Lemma (def) inv_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p\<inverse> \<bullet> p = refl y"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) pathcomp_inv:
+Lemma (def) pathcomp_inv:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p \<bullet> p\<inverse> = refl x"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) pathinv_pathinv:
+Lemma (def) pathinv_pathinv:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p\<inverse>\<inverse> = p"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) pathcomp_assoc:
+Lemma (def) pathcomp_assoc:
   assumes
     "A: U i" "x: A" "y: A" "z: A" "w: A"
     "p: x = y" "q: y = z" "r: z = w"
   shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r"
-  apply (eq p)
-    focus prems vars x p
-      apply (eq p)
-        focus prems vars x p
-          apply (eq p)
-            apply (reduce; intro)
-        done
-    done
-  done
+  proof (eq p)
+    fix x q assuming "x: A" "q: x = z"
+    show "refl x \<bullet> (q \<bullet> r) = refl x \<bullet> q \<bullet> r"
+    proof (eq q)
+      fix x r assuming "x: A" "r: x = w"
+      show "refl x \<bullet> (refl x \<bullet> r) = refl x \<bullet> refl x \<bullet> r"
+        by (eq r) (reduce, refl)
+    qed
+  qed
 
 
 section \<open>Functoriality of functions\<close>
 
-Lemma (derive) ap:
+Lemma (def) ap:
   assumes
     "A: U i" "B: U i"
     "x: A" "y: A"
@@ -213,11 +209,11 @@ definition ap_i ("_[_]" [1000, 0])
 translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
 
 Lemma ap_refl [comp]:
-  assumes "f: A \<rightarrow> B" "x: A" "A: U i" "B: U i"
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A"
   shows "f[refl x] \<equiv> refl (f x)"
   unfolding ap_def by reduce
 
-Lemma (derive) ap_pathcomp:
+Lemma (def) ap_pathcomp:
   assumes
     "A: U i" "B: U i"
     "x: A" "y: A" "z: A"
@@ -225,48 +221,45 @@ Lemma (derive) ap_pathcomp:
     "p: x = y" "q: y = z"
   shows
     "f[p \<bullet> q] = f[p] \<bullet> f[q]"
-  apply (eq p)
-    focus prems vars x p
-      apply (eq p)
-        apply (reduce; intro)
-    done
-  done
+  proof (eq p)
+    fix x q assuming "x: A" "q: x = z"
+    show "f[refl x \<bullet> q] = f[refl x] \<bullet> f[q]"
+      by (eq q) (reduce, refl)
+  qed
 
-Lemma (derive) ap_pathinv:
+Lemma (def) ap_pathinv:
   assumes
     "A: U i" "B: U i"
     "x: A" "y: A"
     "f: A \<rightarrow> B"
     "p: x = y"
   shows "f[p\<inverse>] = f[p]\<inverse>"
-  by (eq p) (reduce; intro)
-
-text \<open>The next two proofs currently use some low-level rewriting.\<close>
+  by (eq p) (reduce, refl)
 
-Lemma (derive) ap_funcomp:
+Lemma (def) ap_funcomp:
   assumes
     "A: U i" "B: U i" "C: U i"
     "x: A" "y: A"
     "f: A \<rightarrow> B" "g: B \<rightarrow> C"
     "p: x = y"
-  shows "(g \<circ> f)[p] = g[f[p]]"
+  shows "(g \<circ> f)[p] = g[f[p]]" thm ap
   apply (eq p)
-    \<guillemotright> by reduce
-    \<guillemotright> by reduce intro
+  \<^item> by reduce
+  \<^item> by reduce refl
   done
 
-Lemma (derive) ap_id:
+Lemma (def) ap_id:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "(id A)[p] = p"
   apply (eq p)
-    \<guillemotright> by reduce
-    \<guillemotright> by reduce intro
+  \<^item> by reduce
+  \<^item> by reduce refl
   done
 
 
 section \<open>Transport\<close>
 
-Lemma (derive) transport:
+Lemma (def) transport:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -288,22 +281,18 @@ Lemma transport_comp [comp]:
   shows "trans P (refl a) \<equiv> id (P a)"
   unfolding transport_def by reduce
 
-\<comment> \<open>TODO: Build transport automation!\<close>
-
-Lemma use_transport:
+Lemma apply_transport:
   assumes
+    "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i"
+    "x: A" "y: A"
     "p: y =\<^bsub>A\<^esub> x"
     "u: P x"
-    "x: A" "y: A"
-    "A: U i"
-    "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "trans P p\<inverse> u: P y"
-  unfolding transport_def pathinv_def
   by typechk
 
-method transport uses eq = (rule use_transport[OF eq])
+method transport uses eq = (rule apply_transport[OF _ _ _ _ eq])
 
-Lemma (derive) transport_left_inv:
+Lemma (def) transport_left_inv:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -312,16 +301,16 @@ Lemma (derive) transport_left_inv:
   shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
   by (eq p) (reduce; refl)
 
-Lemma (derive) transport_right_inv:
+Lemma (def) transport_right_inv:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
     "x: A" "y: A"
     "p: x = y"
   shows "(trans P p) \<circ> (trans P p\<inverse>) = id (P y)"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) transport_pathcomp:
+Lemma (def) transport_pathcomp:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -329,14 +318,14 @@ Lemma (derive) transport_pathcomp:
     "u: P x"
     "p: x = y" "q: y = z"
   shows "trans P q (trans P p u) = trans P (p \<bullet> q) u"
-  apply (eq p)
-    focus prems vars x p
-      apply (eq p)
-        apply (reduce; intro)
-    done
-  done
-
-Lemma (derive) transport_compose_typefam:
+proof (eq p)
+  fix x q u
+  assuming "x: A" "q: x = z" "u: P x"
+  show "trans P q (trans P (refl x) u) = trans P ((refl x) \<bullet> q) u"
+    by (eq q) (reduce, refl)
+qed
+
+Lemma (def) transport_compose_typefam:
   assumes
     "A: U i" "B: U i"
     "\<And>x. x: B \<Longrightarrow> P x: U i"
@@ -345,9 +334,9 @@ Lemma (derive) transport_compose_typefam:
     "p: x = y"
     "u: P (f x)"
   shows "trans (fn x. P (f x)) p u = trans P f[p] u"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) transport_function_family:
+Lemma (def) transport_function_family:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -357,15 +346,15 @@ Lemma (derive) transport_function_family:
     "u: P x"
     "p: x = y"
   shows "trans Q p ((f x) u) = (f y) (trans P p u)"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
-Lemma (derive) transport_const:
+Lemma (def) transport_const:
   assumes
     "A: U i" "B: U i"
     "x: A" "y: A"
     "p: x = y"
   shows "\<Prod>b: B. trans (fn _. B) p b = b"
-  by (intro, eq p) (reduce; intro)
+  by intro (eq p, reduce, refl)
 
 definition transport_const_i ("trans'_const")
   where [implicit]: "trans_const B p \<equiv> transport_const ? B ? ? p"
@@ -376,10 +365,10 @@ Lemma transport_const_comp [comp]:
   assumes
     "x: A" "b: B"
     "A: U i" "B: U i"
-  shows "trans_const B (refl x) b\<equiv> refl b"
+  shows "trans_const B (refl x) b \<equiv> refl b"
   unfolding transport_const_def by reduce
 
-Lemma (derive) pathlift:
+Lemma (def) pathlift:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -387,7 +376,7 @@ Lemma (derive) pathlift:
     "p: x = y"
     "u: P x"
   shows "<x, u> = <y, trans P p u>"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
 definition pathlift_i ("lift")
   where [implicit]: "lift P p u \<equiv> pathlift ? P ? ? p u"
@@ -403,7 +392,7 @@ Lemma pathlift_comp [comp]:
   shows "lift P (refl x) u \<equiv> refl <x, u>"
   unfolding pathlift_def by reduce
 
-Lemma (derive) pathlift_fst:
+Lemma (def) pathlift_fst:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -412,14 +401,14 @@ Lemma (derive) pathlift_fst:
     "p: x = y"
   shows "fst[lift P p u] = p"
   apply (eq p)
-    \<guillemotright> by reduce
-    \<guillemotright> by reduce intro
+  \<^item> by reduce
+  \<^item> by reduce refl
   done
 
 
 section \<open>Dependent paths\<close>
 
-Lemma (derive) apd:
+Lemma (def) apd:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
@@ -427,7 +416,7 @@ Lemma (derive) apd:
     "x: A" "y: A"
     "p: x = y"
   shows "trans P p (f x) = f y"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
 definition apd_i ("apd")
   where [implicit]: "apd f p \<equiv> Identity.apd ? ? f ? ? p"
@@ -443,26 +432,25 @@ Lemma dependent_map_comp [comp]:
   shows "apd f (refl x) \<equiv> refl (f x)"
   unfolding apd_def by reduce
 
-Lemma (derive) apd_ap:
+Lemma (def) apd_ap:
   assumes
     "A: U i" "B: U i"
     "f: A \<rightarrow> B"
     "x: A" "y: A"
     "p: x = y"
   shows "apd f p = trans_const B p (f x) \<bullet> f[p]"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce, refl)
 
 
 section \<open>Whiskering\<close>
 
-Lemma (derive) right_whisker:
+Lemma (def) right_whisker:
   assumes "A: U i" "a: A" "b: A" "c: A"
       and "p: a = b" "q: a = b" "r: b = c"
       and "\<alpha>: p = q"
   shows "p \<bullet> r = q \<bullet> r"
   apply (eq r)
-  focus prems vars x s t
-    proof -
+    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])
@@ -470,14 +458,13 @@ Lemma (derive) right_whisker:
     qed
   done
 
-Lemma (derive) left_whisker:
+Lemma (def) left_whisker:
   assumes "A: U i" "a: A" "b: A" "c: A"
       and "p: b = c" "q: b = c" "r: a = b"
       and "\<alpha>: p = q"
   shows "r \<bullet> p = r \<bullet> q"
   apply (eq r)
-  focus prems prms vars x s t
-    proof -
+    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])
@@ -485,24 +472,24 @@ Lemma (derive) left_whisker:
     qed
   done
 
-definition right_whisker_i (infix "\<bullet>\<^sub>r\<^bsub>_\<^esub>" 121)
-  where [implicit]: "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r \<equiv> right_whisker ? a ? ? ? ? r \<alpha>"
+definition right_whisker_i (infix "\<bullet>\<^sub>r" 121)
+  where [implicit]: "\<alpha> \<bullet>\<^sub>r r \<equiv> right_whisker ? ? ? ? ? ? r \<alpha>"
 
-definition left_whisker_i (infix "\<bullet>\<^sub>l\<^bsub>_\<^esub>" 121)
-  where [implicit]: "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha> \<equiv> left_whisker ? ? ? c ? ? r \<alpha>"
+definition left_whisker_i (infix "\<bullet>\<^sub>l" 121)
+  where [implicit]: "r \<bullet>\<^sub>l \<alpha> \<equiv> left_whisker ? ? ? ? ? ? r \<alpha>"
 
 translations
-  "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>"
-  "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>"
+  "\<alpha> \<bullet>\<^sub>r r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>"
+  "r \<bullet>\<^sub>l \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>"
 
 Lemma whisker_refl [comp]:
   assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q"
-  shows "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
+  shows "\<alpha> \<bullet>\<^sub>r (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
   unfolding right_whisker_def by reduce
 
 Lemma refl_whisker [comp]:
   assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q"
-  shows "(refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
+  shows "(refl a) \<bullet>\<^sub>l \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
   unfolding left_whisker_def by reduce
 
 method left_whisker = (rule left_whisker)
@@ -521,7 +508,7 @@ assumes assums:
   "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
 begin
 
-Lemma (derive) horiz_pathcomp:
+Lemma (def) horiz_pathcomp:
   notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
@@ -532,7 +519,7 @@ qed typechk
 
 text \<open>A second horizontal composition:\<close>
 
-Lemma (derive) horiz_pathcomp':
+Lemma (def) horiz_pathcomp':
   notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
@@ -544,14 +531,14 @@ qed typechk
 notation horiz_pathcomp (infix "\<star>" 121)
 notation horiz_pathcomp' (infix "\<star>''" 121)
 
-Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp':
+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 _ q by (eq q) (reduce; refl)
+      focus vars a q by (eq q) (reduce, refl)
     done
   done
 
@@ -580,12 +567,20 @@ interpretation \<Omega>2:
 notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
 notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
 
-Lemma (derive) pathcomp_eq_horiz_pathcomp:
+Lemma [typechk]:
+  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"
+  using assms
+  unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_alt_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
   using assms[unfolded \<Omega>2_alt_def]
-  proof (reduce, rule pathinv) 
+  proof (reduce, rule pathinv)
     \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
     have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
     also have ".. = \<alpha>" by (rule refl_pathcomp)
@@ -596,12 +591,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp:
     finally have eq\<beta>: "{} = \<beta>" by this
 
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
-      = \<alpha> \<bullet> {}" by right_whisker (rule eq\<alpha>)
-    also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (rule eq\<beta>)
+      = \<alpha> \<bullet> {}" by right_whisker (fact eq\<alpha>)
+    also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>)
     finally show "{} = \<alpha> \<bullet> \<beta>" by this
   qed
 
-Lemma (derive) pathcomp_eq_horiz_pathcomp':
+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
@@ -616,12 +611,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp':
     finally have eq\<alpha>: "{} = \<alpha>" by this
 
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
-      = \<beta> \<bullet> {}" by right_whisker (rule eq\<beta>)
-    also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (rule eq\<alpha>)
+      = \<beta> \<bullet> {}" by right_whisker (fact eq\<beta>)
+    also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>)
     finally show "{} = \<beta> \<bullet> \<alpha>" by this
   qed
 
-Lemma (derive) eckmann_hilton:
+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]
@@ -629,11 +624,15 @@ Lemma (derive) eckmann_hilton:
     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>
       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.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def)+
+      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>
   qed
 
 end
diff --git a/hott/More_List.thy b/hott/List+.thy
index 1b8034f..b73cc24 100644
--- a/hott/More_List.thy
+++ b/hott/List+.thy
@@ -1,4 +1,4 @@
-theory More_List
+theory "List+"
 imports
   Spartan.List
   Nat
@@ -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)
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)
 end
 
 
diff --git a/hott/More_Nat.thy b/hott/More_Nat.thy
deleted file mode 100644
index 59c8d54..0000000
--- a/hott/More_Nat.thy
+++ /dev/null
@@ -1,43 +0,0 @@
-theory More_Nat
-imports Nat Spartan.More_Types
-
-begin
-
-section \<open>Equality on Nat\<close>
-
-text \<open>Via the encode-decode method.\<close>
-
-context begin
-
-Lemma (derive) eq: shows "Nat \<rightarrow> Nat \<rightarrow> U O"
-  apply intro focus vars m apply elim
-    \<comment> \<open>m \<equiv> 0\<close>
-    apply intro focus vars n apply elim
-      \<guillemotright> by (rule TopF) \<comment> \<open>n \<equiv> 0\<close>
-      \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> suc _\<close>
-      \<guillemotright> by (rule Ui_in_USi)
-    done
-    \<comment> \<open>m \<equiv> suc k\<close>
-    apply intro focus vars k k_eq n apply (elim n)
-      \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> 0\<close>
-      \<guillemotright> prems vars l proof - show "k_eq l: U O" by typechk qed
-      \<guillemotright> by (rule Ui_in_USi)
-    done
-    by (rule Ui_in_USi)
-  done
-
-text \<open>
-\<^term>\<open>eq\<close> is defined by
-  eq 0 0 \<equiv> \<top>
-  eq 0 (suc k) \<equiv> \<bottom>
-  eq (suc k) 0 \<equiv> \<bottom>
-  eq (suc k) (suc l) \<equiv> eq k l
-\<close>
-
-
-
-
-end
-
-
-end
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 177ec47..fd567f3 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -77,43 +77,43 @@ lemma add_suc [comp]:
   shows "m + suc n \<equiv> suc (m + n)"
   unfolding add_def by reduce
 
-Lemma (derive) zero_add:
+Lemma (def) zero_add:
   assumes "n: Nat"
   shows "0 + n = n"
   apply (elim n)
-    \<guillemotright> by (reduce; intro)
-    \<guillemotright> vars _ ih by reduce (eq ih; intro)
+    \<^item> by (reduce; intro)
+    \<^item> vars _ ih by reduce (eq ih; refl)
   done
 
-Lemma (derive) suc_add:
+Lemma (def) suc_add:
   assumes "m: Nat" "n: Nat"
   shows "suc m + n = suc (m + n)"
   apply (elim n)
-    \<guillemotright> by reduce refl
-    \<guillemotright> vars _ ih by reduce (eq ih; intro)
+    \<^item> by reduce refl
+    \<^item> vars _ ih by reduce (eq ih; refl)
   done
 
-Lemma (derive) suc_eq:
+Lemma (def) suc_eq:
   assumes "m: Nat" "n: Nat"
   shows "p: m = n \<Longrightarrow> suc m = suc n"
   by (eq p) intro
 
-Lemma (derive) add_assoc:
+Lemma (def) add_assoc:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l + (m + n) = l + m+ n"
   apply (elim n)
-    \<guillemotright> by reduce intro
-    \<guillemotright> vars _ ih by reduce (eq ih; intro)
+    \<^item> by reduce intro
+    \<^item> vars _ ih by reduce (eq ih; refl)
   done
 
-Lemma (derive) add_comm:
+Lemma (def) add_comm:
   assumes "m: Nat" "n: Nat"
   shows "m + n = n + m"
   apply (elim n)
-    \<guillemotright> by (reduce; rule zero_add[symmetric])
-    \<guillemotright> prems vars n ih
+    \<^item> by (reduce; rule zero_add[symmetric])
+    \<^item> vars n ih
       proof reduce
-        have "suc (m + n) = suc (n + m)" by (eq ih) intro
+        have "suc (m + n) = suc (n + m)" by (eq ih) refl
         also have ".. = suc n + m" by (transport eq: suc_add) refl
         finally show "{}" by this
       qed
@@ -143,12 +143,12 @@ lemma mul_suc [comp]:
   shows "m * suc n \<equiv> m + m * n"
   unfolding mul_def by reduce
 
-Lemma (derive) zero_mul:
+Lemma (def) zero_mul:
   assumes "n: Nat"
   shows "0 * n = 0"
   apply (elim n)
-  \<guillemotright> by reduce refl
-  \<guillemotright> prems vars n ih
+  \<^item> by reduce refl
+  \<^item> vars n ih
     proof reduce
       have "0 + 0 * n = 0 + 0 " by (eq ih) refl
       also have ".. = 0" by reduce refl
@@ -156,12 +156,12 @@ Lemma (derive) zero_mul:
     qed
   done
 
-Lemma (derive) suc_mul:
+Lemma (def) suc_mul:
   assumes "m: Nat" "n: Nat"
   shows "suc m * n = m * n + n"
   apply (elim n)
-  \<guillemotright> by reduce refl
-  \<guillemotright> prems vars n ih
+  \<^item> by reduce refl
+  \<^item> vars n ih
     proof (reduce, transport eq: \<open>ih:_\<close>)
       have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add)
       also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl
@@ -169,12 +169,12 @@ Lemma (derive) suc_mul:
     qed
   done
 
-Lemma (derive) mul_dist_add:
+Lemma (def) mul_dist_add:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l * (m + n) = l * m + l * n"
   apply (elim n)
-  \<guillemotright> by reduce refl
-  \<guillemotright> prems prms vars n ih
+  \<^item> by reduce refl
+  \<^item> vars n ih
     proof reduce
       have "l + l * (m + n) = l + (l * m + l * n)" by (eq ih) refl
       also have ".. = l + l * m + l * n" by (rule add_assoc)
@@ -184,12 +184,12 @@ Lemma (derive) mul_dist_add:
     qed
   done
 
-Lemma (derive) mul_assoc:
+Lemma (def) mul_assoc:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l * (m * n) = l * m * n"
   apply (elim n)
-  \<guillemotright> by reduce refl
-  \<guillemotright> prems vars n ih
+  \<^item> by reduce refl
+  \<^item> vars n ih
     proof reduce
       have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add)
       also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl
@@ -197,12 +197,12 @@ Lemma (derive) mul_assoc:
     qed
   done
 
-Lemma (derive) mul_comm:
+Lemma (def) mul_comm:
   assumes "m: Nat" "n: Nat"
   shows "m * n = n * m"
   apply (elim n)
-  \<guillemotright> by reduce (transport eq: zero_mul, refl)
-  \<guillemotright> prems vars n ih
+  \<^item> by reduce (transport eq: zero_mul, refl)
+  \<^item> vars n ih
     proof (reduce, rule pathinv)
       have "suc n * m = n * m + m" by (rule suc_mul)
       also have ".. = m + m * n"
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index faa692d..27edd51 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -8,9 +8,9 @@ imports
 keywords
   "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
   "assuming" :: prf_asm % "proof" and
-  "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
+  "focus" "\<^item>" "\<^enum>" "\<circ>" "\<diamondop>" "~" :: prf_script_goal % "proof" and
   "congruence" "print_coercions" :: thy_decl and
-  "rhs" "derive" "prems" "vars" :: quasi_command
+  "rhs" "def" "vars" :: quasi_command
 
 begin
 
@@ -198,8 +198,8 @@ lemmas
   [form] = PiF SigF and
   [intro] = PiI SigI and
   [intros] = PiI[rotated] SigI and
-  [elim "?f"] = PiE and
-  [elim "?p"] = SigE and
+  [elim ?f] = PiE and
+  [elim ?p] = SigE and
   [comp] = beta Sig_comp and
   [cong] = Pi_cong lam_cong Sig_cong
 
@@ -217,7 +217,7 @@ subsection \<open>Statement commands\<close>
 
 ML_file \<open>focus.ML\<close>
 ML_file \<open>elaboration.ML\<close>
-ML_file \<open>elaborated_assumption.ML\<close>
+ML_file \<open>elaborated_statement.ML\<close>
 ML_file \<open>goals.ML\<close>
 
 subsection \<open>Proof methods\<close>
@@ -229,10 +229,6 @@ method_setup rule =
   \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
     CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
 
-method_setup rules =
-  \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
-    CREPEAT o 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 (
@@ -411,10 +407,10 @@ lemma funcompI [typechk]:
 
 lemma funcomp_assoc [comp]:
   assumes
+    "A: U i"
     "f: A \<rightarrow> B"
     "g: B \<rightarrow> C"
     "h: \<Prod>x: C. D x"
-    "A: U i"
   shows
     "(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
@@ -430,10 +426,9 @@ lemma funcomp_lambda_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"
     "x: A"
-    "A: U i" "B: U i"
-    "\<And>x y. x: B \<Longrightarrow> C x: U i"
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
   unfolding funcomp_def by reduce
 
@@ -449,17 +444,17 @@ subsection \<open>Identity function\<close>
 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_type [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
   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]:
-  assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+  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]:
-  assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+  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)
 
@@ -480,10 +475,7 @@ lemma fst_type [typechk]:
 
 lemma fst_comp [comp]:
   assumes
-    "a: A"
-    "b: B a"
-    "A: U i"
-    "\<And>x. x: A \<Longrightarrow> B x: U i"
+    "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
 
@@ -493,7 +485,7 @@ lemma snd_type [typechk]:
   unfolding snd_def by typechk reduce
 
 lemma snd_comp [comp]:
-  assumes "a: A" "b: B a" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+  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
 
@@ -513,36 +505,48 @@ subsection \<open>Projections\<close>
 
 Lemma fst [typechk]:
   assumes
-    "p: \<Sum>x: A. B x"
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+    "p: \<Sum>x: A. B x"
   shows "fst p: A"
   by typechk
 
 Lemma snd [typechk]:
   assumes
-    "p: \<Sum>x: A. B x"
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+    "p: \<Sum>x: A. B x"
   shows "snd p: B (fst p)"
   by typechk
 
-method fst for p::o = rule fst[of p]
-method snd for p::o = rule snd[of p]
+method fst for p::o = rule fst[where ?p=p]
+method snd for p::o = rule snd[where ?p=p]
 
-subsection \<open>Properties of \<Sigma>\<close>
+text \<open>Double projections:\<close>
 
-Lemma (derive) Sig_dist_exp:
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.fst ? ? p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.fst ? ? p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.snd ? ? p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.snd ? ? p)"
+
+translations
+  "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
+  "CONST p\<^sub>1\<^sub>2 p" \<leftharpoondown> "snd (fst p)"
+  "CONST p\<^sub>2\<^sub>1 p" \<leftharpoondown> "fst (snd p)"
+  "CONST p\<^sub>2\<^sub>2 p" \<leftharpoondown> "snd (snd p)"
+
+Lemma (def) distribute_Sig:
   assumes
-    "p: \<Sum>x: A. B x \<times> C x"
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> B x: U i"
     "\<And>x. x: A \<Longrightarrow> C x: U i"
+    "p: \<Sum>x: A. B x \<times> C x"
   shows "(\<Sum>x: A. B x) \<times> (\<Sum>x: A. C x)"
-proof intro
-  have "fst p: A" and "snd p: B (fst p) \<times> C (fst p)" by typechk+
-  thus "<fst p, fst (snd p)>: \<Sum>x: A. B x"
-   and "<fst p, snd (snd p)>: \<Sum>x: A. C x"
-    by typechk+
-qed
+  proof intro
+    have "fst p: A" and "snd p: B (fst p) \<times> C (fst p)"
+      by typechk+
+    thus "<fst p, fst (snd p)>: \<Sum>x: A. B x"
+     and "<fst p, snd (snd p)>: \<Sum>x: A. C x"
+      by typechk+
+  qed
 
 
 end
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
index a5159f6..b5a6c00 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -2,6 +2,10 @@
     Author:     Joshua Chen
 
 More context tactics, and context tactic combinators.
+
+Contains code modified from
+  ~~/Pure/search.ML
+  ~~/Pure/tactical.ML
 *)
 
 infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
@@ -23,6 +27,7 @@ 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 CREPEAT1: 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'
@@ -34,6 +39,16 @@ 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'
+val CFIRST: context_tactic list -> context_tactic
+val CFIRST': context_tactic' list -> context_tactic'
+val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) ->
+  (context_state -> int) -> context_tactic -> context_tactic
+val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) ->
+  context_tactic -> context_tactic
+val CTHEN_ASTAR: context_tactic -> (context_state -> bool) ->
+  (int -> context_state -> int) -> context_tactic -> context_tactic
+val CASTAR: (context_state -> bool) -> (int -> context_state -> int) ->
+  context_tactic -> context_tactic
 
 end = struct
 
@@ -74,6 +89,8 @@ fun CREPEAT ctac =
           | SOME (cst, q) => rep (q :: qs) cst);
   in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end
 
+fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
+
 fun CFILTER pred ctac cst =
   ctac cst
   |> Seq.filter_results
@@ -147,6 +164,89 @@ fun CSOMEGOAL ctac (cst as (_, st)) =
 fun CRANGE [] _ = all_ctac
   | CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i
 
+fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac
+
+(*FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i*)
+fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac)
+
+
+(** Search tacticals **)
+
+(* Best-first search *)
+
+structure Thm_Heap = Heap (
+  type elem = int * thm;
+  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of)
+)
+
+structure Context_State_Heap = Heap (
+  type elem = int * context_state;
+  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2))
+)
+
+fun some_of_list [] = NONE
+  | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l))
+
+(*Check for and delete duplicate proof states*)
+fun delete_all_min (cst as (_, st)) heap =
+  if Context_State_Heap.is_empty heap then heap
+  else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap)))
+  then delete_all_min cst (Context_State_Heap.delete_min heap)
+  else heap
+
+(*Best-first search for a state that satisfies satp (incl initial state)
+  Function sizef estimates size of problem remaining (smaller means better).
+  tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
+fun CTHEN_BEST_FIRST ctac0 satp sizef ctac =
+  let
+    fun pairsize cst = (sizef cst, cst);
+    fun bfs (news, nst_heap) =
+      (case List.partition satp news of
+        ([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap)
+      | (sats, _)  => some_of_list sats)
+    and next nst_heap =
+      if Context_State_Heap.is_empty nst_heap then NONE
+      else
+        let
+          val (n, cst) = Context_State_Heap.min nst_heap;
+        in
+          bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap))
+        end;
+    fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty)
+  in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end
+
+(*Ordinary best-first search, with no initial tactic*)
+val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac
+
+
+(* A*-like search *)
+
+(*Insertion into priority queue of states, marked with level*)
+fun insert_with_level (lnth: int * int * context_state) [] = [lnth]
+  | insert_with_level (l, m, cst) ((l', n, cst') :: csts) =
+      if  n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts
+      else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts
+      else (l, m, cst) :: (l', n, cst') :: csts;
+
+fun CTHEN_ASTAR ctac0 satp costf ctac =
+  let
+    fun bfs (news, nst, level) =
+      let fun cost cst = (level, costf level cst, cst) in
+        (case List.partition satp news of
+          ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst)
+        | (sats, _) => some_of_list sats)
+      end
+    and next [] = NONE
+      | next ((level, n, cst) :: nst) =
+          bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1)
+  in fn cst => Seq.make_results
+    (Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0)))
+  end
+
+(*Ordinary ASTAR, with no initial tactic*)
+val CASTAR = CTHEN_ASTAR all_ctac;
+
+
 end
 
 open Context_Tactical
diff --git a/spartan/core/elaborated_assumption.ML b/spartan/core/elaborated_statement.ML
index af3a384..81f4a7d 100644
--- a/spartan/core/elaborated_assumption.ML
+++ b/spartan/core/elaborated_statement.ML
@@ -1,7 +1,7 @@
-(*  Title:      elaborated_assumption.ML
+(*  Title:      elaborated_statement.ML
     Author:     Joshua Chen
 
-Term elaboration for goal and proof assumptions.
+Term elaboration for goal statements and proof commands.
 
 Contains code from parts of
   ~~/Pure/Isar/element.ML and
@@ -9,7 +9,7 @@ Contains code from parts of
 in both verbatim and modified forms.
 *)
 
-structure Elaborated_Assumption: sig
+structure Elaborated_Statement: sig
 
 val read_goal_statement:
   (string, string, Facts.ref) Element.ctxt list ->
@@ -20,24 +20,7 @@ val read_goal_statement:
 end = struct
 
 
-(*Apply elaboration to the list format assumptions are given in*)
-fun elaborate ctxt assms =
-  let
-    fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
-    fun elab_fact (fact, xs) assums =
-      let val (subst, fact') = Elab.elab_stmt ctxt assums fact in
-        ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
-      end
-    fun elab (b, facts) assums =
-      let val (facts', assums') = fold_map elab_fact facts assums
-      in ((b, facts'), assums') end
-  in #1 (fold_map elab assms []) end
-
-
-(* Goal assumptions *)
-
-(*Most of the code in this section is copied verbatim from the originals; the
-  only change is a modification to`activate_i` incorporating elaboration.*)
+(* Elaborated goal statements *)
 
 local
 
@@ -371,16 +354,28 @@ val read_full_context_statement = prep_full_context_statement
   Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src
   Proof_Context.read_var check_expr
 
+fun filter_assumes ((x as Element.Assumes _) :: xs) = x :: filter_assumes xs
+  | filter_assumes (_ :: xs) = filter_assumes xs
+  | filter_assumes [] = []
+
 fun prep_statement prep activate raw_elems raw_stmt ctxt =
   let
     val ((_, _, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
-        ([], []) I raw_elems raw_stmt ctxt;
-    val ctxt' = ctxt
+        ([], []) I raw_elems raw_stmt ctxt
+
+    val (elems', ctxt') = ctxt
       |> Proof_Context.set_stmt true
-      |> fold_map activate elems |> #2
-      |> Proof_Context.restore_stmt ctxt;
-  in (concl, ctxt') end
+      |> fold_map activate elems
+      |> apsnd (Proof_Context.restore_stmt ctxt)
+
+    val assumes = filter_assumes elems'
+    val assms = flat (flat (map
+      (fn (Element.Assumes asms) =>
+        map (fn (_, facts) => map (Thm.cterm_of ctxt' o #1) facts) asms)
+      assumes))
+    val concl' = Elab.elaborate ctxt' assms concl handle error => concl
+  in (concl', ctxt') end
 
 fun activate_i elem ctxt =
   let
@@ -391,7 +386,7 @@ fun activate_i elem ctxt =
             ((Thm.def_binding_optional
               (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
               (t, ps))))
-      | Element.Assumes assms => Element.Assumes (elaborate ctxt assms)
+      | Element.Assumes assms => Element.Assumes (Elab.elaborate ctxt [] assms)
       | e => e);
     val ctxt' = Context.proof_map (Element.init elem') ctxt;
   in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end
@@ -437,7 +432,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elabora
       val b' = map (map read_terms) b
       val c' = c |> map (fn ((b, atts), ss) =>
         ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss))
-      val c'' = elaborate ctxt c'
+      val c'' = Elab.elaborate ctxt [] c'
     in Proof.assume a' b' c'' state end)))
 
 end
diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML
index 27b6bb0..9e5e0bd 100644
--- a/spartan/core/elaboration.ML
+++ b/spartan/core/elaboration.ML
@@ -1,13 +1,14 @@
 (*  Title:      elaboration.ML
     Author:     Joshua Chen
 
-Basic elaboration.
+Basic term elaboration.
 *)
 
 structure Elab: sig
 
 val elab: Proof.context -> cterm list -> term -> Envir.env
 val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
+val elaborate: Proof.context -> cterm list -> ('a * (term * term list) list) list -> ('a * (term * term list) list) list
 
 end = struct
 
@@ -72,5 +73,19 @@ fun elab_stmt ctxt assums stmt =
       in (subst', subst_term subst' stmt) end
   end
 
+(*Apply elaboration to the list format that assumptions and goal statements are
+  given in*)
+fun elaborate ctxt known assms =
+  let
+    fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
+    fun elab_fact (fact, xs) assums =
+      let val (subst, fact') = elab_stmt ctxt assums fact in
+        ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
+      end
+    fun elab (b, facts) assums =
+      let val (facts', assums') = fold_map elab_fact facts assums
+      in ((b, facts'), assums') end
+  in #1 (fold_map elab assms known) end
+
 
 end
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML
index 1d8de78..2ad4c8a 100644
--- a/spartan/core/focus.ML
+++ b/spartan/core/focus.ML
@@ -1,14 +1,51 @@
 (*  Title:      focus.ML
-    Author:     Makarius Wenzel, Joshua Chen
+    Author:     Joshua Chen
 
-A modified version of the Isar `subgoal` command
-that keeps schematic variables in the goal state.
+Focus on head subgoal, with optional variable renaming.
 
-Modified from code originally written by Makarius Wenzel.
+Modified from code contained in ~~/Pure/Isar/subgoal.ML.
 *)
 
 local
 
+fun reverse_prems imp =
+  let val (prems, concl) = (Drule.strip_imp_prems imp, Drule.strip_imp_concl imp)
+  in fold (curry mk_implies) prems concl end
+
+fun gen_focus ctxt i bindings raw_st =
+  let
+    val st = raw_st
+      |> Thm.solve_constraints
+      |> Thm.transfer' ctxt
+      |> Raw_Simplifier.norm_hhf_protect ctxt
+
+    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt
+
+    val ((params, goal), ctxt2) =
+      Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1
+
+    val (asms, concl) =
+      (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+
+    fun intern_var_assms asm (asms, concl) =
+      if Lib.no_vars (Thm.term_of asm)
+      then (asm :: asms, concl)
+      else (asms, Drule.mk_implies (asm, concl))
+
+    val (asms', concl') = fold intern_var_assms asms ([], concl)
+      |> apfst rev |> apsnd reverse_prems
+
+    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2
+    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst)
+    val schematics = (schematic_types, schematic_terms)
+    val asms' = map (Thm.instantiate_cterm schematics) asms'
+    val concl' = Thm.instantiate_cterm schematics concl'
+    val (prems, context) = Assumption.add_assumes asms' ctxt3
+  in
+    ({context = context, params = params, prems = prems,
+      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
+  end
+
 fun param_bindings ctxt (param_suffix, raw_param_specs) st =
   let
     val _ = if Thm.no_prems st then error "No subgoals!" else ()
@@ -24,8 +61,8 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st =
         error ("Excessive subgoal parameter specification" ^
           Position.here_list (map snd (drop n raw_param_specs)))
 
-    val param_specs =
-      raw_param_specs |> map
+    val param_specs = raw_param_specs
+      |> map
         (fn (NONE, _) => NONE
           | (SOME x, pos) =>
               let
@@ -39,7 +76,7 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st =
       | bindings _ ys = map Binding.name ys
   in bindings param_specs subgoal_params end
 
-fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state =
   let
     val _ = Proof.assert_backward state
 
@@ -47,17 +84,13 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s
       |> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic)
       |> Proof.refine_insert []
 
-    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1
-
+    val {context = ctxt, facts, goal = st} = Proof.raw_goal state1
     val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding
-    val (prems_binding, do_prems) =
-      (case raw_prems_binding of
-        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
-      | NONE => (Binding.empty_atts, false))
 
-    val (subgoal_focus, _) =
-      (if do_prems then Subgoal.focus_prems else Subgoal.focus_params) ctxt
-        1 (SOME (param_bindings ctxt param_specs st)) st
+    val subgoal_focus = #1
+      (gen_focus ctxt 1 (SOME (param_bindings ctxt param_specs st)) st)
+
+    val prems = #prems subgoal_focus
 
     fun after_qed (ctxt'', [[result]]) =
       Proof.end_block #> (fn state' =>
@@ -83,31 +116,29 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s
     |> Proof.begin_block
     |> Proof.map_context (fn _ =>
       #context subgoal_focus
-      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+      |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])]
+      |> #2)
     |> 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
-    |> Proof.using_facts facts
+        NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])]
+    |> #2
+    |> Proof.using_facts (facts @ prems)
     |> pair subgoal_focus
   end
 
 val opt_fact_binding =
-  Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+  Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Args.colon)
     Binding.empty_atts
 
-val for_params =
-  Scan.optional
-    (\<^keyword>\<open>vars\<close> |--
-      Parse.!!! ((Scan.option Parse.dots >> is_some) --
-        (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
-    (false, [])
+val for_params = Scan.optional
+  (\<^keyword>\<open>vars\<close> |--
+    Parse.!!! ((Scan.option Parse.dots >> is_some) --
+      (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
+  (false, [])
 
 val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
 
-val parser =
-  opt_fact_binding
-  -- (Scan.option (\<^keyword>\<open>prems\<close> |-- Parse.!!! opt_fact_binding))
-  -- for_params >> (fn ((a, b), c) =>
-    Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c))
+val parser = opt_fact_binding -- for_params >> (fn (fact, params) =>
+  Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd fact params))
 
 in
 
@@ -117,9 +148,10 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>focus\<close>
   "focus on first subgoal within backward refinement, without instantiating schematic vars"
   parser
 
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<guillemotright>\<close> "focus bullet" parser
 val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^item>\<close> "focus bullet" parser
 val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^enum>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<circ>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<diamondop>\<close> "focus bullet" parser
 val _ = Outer_Syntax.command \<^command_keyword>\<open>~\<close> "focus bullet" parser
 
 end
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 87ec2b8..540f5c7 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -1,9 +1,9 @@
 (*  Title:      goals.ML
-    Author:     Makarius Wenzel, Joshua Chen
+    Author:     Joshua Chen
 
 Goal statements and proof term export.
 
-Modified from code originally written by Makarius Wenzel.
+Modified from code contained in ~~/Pure/Isar/specification.ML.
 *)
 
 local
@@ -184,15 +184,15 @@ val schematic_theorem_cmd =
   gen_schematic_theorem
     Bundle.includes_cmd
     Attrib.check_src
-    Elaborated_Assumption.read_goal_statement
+    Elaborated_Statement.read_goal_statement
 
 fun theorem spec descr =
   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
-    ( Scan.option (Args.parens (Args.$$$ "derive"))
+    ( 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 "derive" => true | _ => false)
+            (case opt_derive of SOME "def" => true | _ => false)
             long descr NONE (K I) binding includes elems concl) )
 
 fun definition spec descr =
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 3922ae0..19d3d71 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -19,8 +19,7 @@ end = struct
 
 
 (* Side conditions *)
-val solve_side_conds =
-  Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
+val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
 
 fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN
   (case Config.get ctxt solve_side_conds of
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index 57164a1..a6e1726 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -51,10 +51,9 @@ 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 = facts
+        let val ths = map (Simplifier.norm_hhf ctxt)
+          (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
           (*FIXME: Shouldn't pull nameless facts directly from context*)
-          @ map fst (Facts.props (Proof_Context.facts_of ctxt))
-          |> map (Simplifier.norm_hhf ctxt)
         in
           (debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE
           debug_tac ctxt "assume" THEN assume_tac ctxt i) st
@@ -70,7 +69,8 @@ fun check_infer_step facts i (ctxt, st) =
     val tac = SUBGOAL (fn (goal, i) =>
       if Lib.rigid_typing_concl goal
       then
-        let val net = Tactic.build_net (facts
+        let val net = Tactic.build_net (
+          map (Simplifier.norm_hhf ctxt) 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>)
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index be86b63..34873e4 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -132,9 +132,9 @@ Definition app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (fact \<open>ys:_\<close>)
-  \<guillemotright> prems vars x _ rec
-    proof - show "x # rec: List A" by typechk qed
+    \<^item> by (fact \<open>ys:_\<close>)
+    \<^item> vars x _ rec
+      proof - show "x # rec: List A" by typechk qed
   done
 
 definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
@@ -169,8 +169,8 @@ Definition rev:
   assumes "A: U i" "xs: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (rule List_nil)
-  \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
+    \<^item> by (rule List_nil)
+    \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
 definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 0ce534c..a2e1638 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -1,7 +1,7 @@
 chapter \<open>Maybe type\<close>
 
 theory Maybe
-imports More_Types
+imports Prelude
 
 begin
 
@@ -25,11 +25,10 @@ Definition MaybeInd:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
   shows "C m"
-  supply assms[unfolded Maybe_def none_def some_def]
+  using assms[unfolded Maybe_def none_def some_def]
   apply (elim m)
-  \<guillemotright> unfolding Maybe_def .
-  \<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
-  \<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
+    apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
+    apply (elim, rule \<open>_: C (inr _ _ _)\<close>)
   done
 
 Lemma Maybe_comp_none:
@@ -39,8 +38,9 @@ Lemma Maybe_comp_none:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def none_def by reduce
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 Lemma Maybe_comp_some:
   assumes
@@ -50,8 +50,9 @@ Lemma Maybe_comp_some:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/Prelude.thy
index 55e6554..36f12d2 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/Prelude.thy
@@ -1,4 +1,4 @@
-theory More_Types
+theory Prelude
 imports Spartan
 
 begin
@@ -114,7 +114,7 @@ Lemma if_true:
     "b: C false"
   shows "ifelse C true a b \<equiv> a"
   unfolding ifelse_def true_def
-  supply assms[unfolded Bool_def true_def false_def]
+  using assms unfolding Bool_def true_def false_def
   by reduce
 
 Lemma if_false:
@@ -124,7 +124,7 @@ Lemma if_false:
     "b: C false"
   shows "ifelse C false a b \<equiv> b"
   unfolding ifelse_def false_def
-  supply assms[unfolded Bool_def true_def false_def]
+  using assms unfolding Bool_def true_def false_def
   by reduce
 
 lemmas