9 files changed, 154 insertions, 158 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 379dc81..9fe11a7 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -88,12 +88,12 @@ lemmas
 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"
-  by reduce
+  by compute
 
 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"
-  by reduce
+  by compute
 
 Lemma funcomp_left_htpy:
   assumes
@@ -105,7 +105,7 @@ Lemma funcomp_left_htpy:
     "H: g ~ g'"
   shows "(g \<circ> f) ~ (g' \<circ> f)"
   unfolding homotopy_def
-  apply (intro, reduce)
+  apply (intro, compute)
   apply (htpy H)
   done
 
@@ -118,12 +118,12 @@ Lemma funcomp_right_htpy:
     "H: f ~ f'"
   shows "(g \<circ> f) ~ (g \<circ> f')"
   unfolding homotopy_def
-  proof (intro, reduce)
+  proof (intro, compute)
     fix x assuming "x: A"
     have *: "f x = f' x"
       by (htpy H)
     show "g (f x) = g (f' x)"
-      by (transport eq: *) refl
+      by (rewr eq: *) refl
   qed
 
 method lhtpy = rule funcomp_left_htpy[rotated 6]
@@ -139,8 +139,8 @@ Lemma (def) commute_homotopy:
   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)
+  apply (eq p, compute)
+  apply (rewr eq: pathcomp_refl, rewr eq: refl_pathcomp)
   by refl
 
 Corollary (def) commute_homotopy':
@@ -151,21 +151,13 @@ Corollary (def) commute_homotopy':
     "H: f ~ (id A)"
   shows "H (f x) = f [H x]"
   proof -
-    (* Rewrite the below proof
-    have *: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
-      using \<open>H:_\<close> unfolding homotopy_def by (rule commute_homotopy)
-
-    thus "H (f x) = f[H x]"
-      apply (pathcomp_cancelr)
-      ...
-    *)
-    (*FUTURE: Because we don't have very good normalization integrated into
+   (*FUTURE: Because we don't have very good normalization integrated into
       things yet, we need to manually unfold the type of H.*)
     from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
-      by (reduce add: homotopy_def)
+      by (compute add: homotopy_def)
 
     have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
-      by (rule left_whisker, transport eq: ap_id, refl)
+      by (rule left_whisker, rewr eq: ap_id, refl)
     also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
       by (rule commute_homotopy)
     finally have "?" by this
@@ -198,7 +190,7 @@ Lemma (def) id_is_qinv:
   unfolding is_qinv_def
   proof intro
     show "id A: A \<rightarrow> A" by typechk
-  qed (reduce, intro; refl)
+  qed (compute, intro; refl)
 
 Lemma is_qinvI:
   assumes
@@ -245,17 +237,17 @@ Lemma (def) funcomp_is_qinv:
     \<^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
+          have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by compute refl
           also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact
-          also have ".. ~ id A" by reduce fact
+          also have ".. ~ id A" by compute 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
+          have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by compute refl
           also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact
-          also have ".. ~ id C" by reduce fact
+          also have ".. ~ id C" by compute fact
           finally show "?" by this
         qed
       qed
@@ -317,10 +309,10 @@ Lemma (def) is_qinv_if_is_biinv:
       \<^item> by (fact \<open>g: _\<close>)
       \<^item> by (fact \<open>H1: _\<close>)
       \<^item> proof -
-          have "g ~ g \<circ> (id B)" by reduce refl
+          have "g ~ g \<circ> (id B)" by compute 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
+          also have ".. ~ (id A) \<circ> h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact)
+          also have ".. ~ h" by compute refl
           finally have "g ~ h" by this
           then have "f \<circ> g ~ f \<circ> h" by (rhtpy, this)
           also note \<open>H2:_\<close>
@@ -420,24 +412,24 @@ Lemma (def) equiv_if_equal:
   apply intro defer
     \<^item> apply (eq p)
       \<^enum> vars A B
-        apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
+        apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
         using [[solve_side_conds=1]]
-        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+        apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
         apply (rule transport, rule Ui_in_USi)
         by (rule lift_universe_codomain, rule Ui_in_USi)
       \<^enum> vars A
         using [[solve_side_conds=1]]
-        apply (rewrite transport_comp)
+        apply (comp transport_comp)
           \<circ> by (rule Ui_in_USi)
-          \<circ> by reduce (rule U_lift)
-          \<circ> by reduce (rule id_is_biinv)
+          \<circ> by compute (rule U_lift)
+          \<circ> by compute (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])
+      apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
       using [[solve_side_conds=1]]
-      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+      apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
       apply (rule transport, rule Ui_in_USi)
       by (rule lift_universe_codomain, rule Ui_in_USi)
   done
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 0a31dc7..caab2e3 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -85,7 +85,7 @@ Lemma (def) pathinv:
 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
+  unfolding pathinv_def by compute
 
 Lemma (def) pathcomp:
   assumes
@@ -101,7 +101,7 @@ Lemma (def) pathcomp:
 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
+  unfolding pathcomp_def by compute
 
 method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
 
@@ -137,12 +137,12 @@ section \<open>Basic propositional equalities\<close>
 Lemma (def) refl_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "(refl x) \<bullet> p = p"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) pathcomp_refl:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p \<bullet> (refl y) = p"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 definition [implicit]: "lu p \<equiv> refl_pathcomp {} {} {} p"
 definition [implicit]: "ru p \<equiv> pathcomp_refl {} {} {} p"
@@ -154,27 +154,27 @@ translations
 Lemma lu_refl [comp]:
   assumes "A: U i" "x: A"
   shows "lu (refl x) \<equiv> refl (refl x)"
-  unfolding refl_pathcomp_def by reduce
+  unfolding refl_pathcomp_def by compute
 
 Lemma ru_refl [comp]:
   assumes "A: U i" "x: A"
   shows "ru (refl x) \<equiv> refl (refl x)"
-  unfolding pathcomp_refl_def by reduce
+  unfolding pathcomp_refl_def by compute
 
 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, refl)
+  by (eq p) (compute, refl)
 
 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, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) pathinv_pathinv:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "p\<inverse>\<inverse> = p"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) pathcomp_assoc:
   assumes
@@ -187,7 +187,7 @@ Lemma (def) pathcomp_assoc:
     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)
+        by (eq r) (compute, refl)
     qed
   qed
 
@@ -211,7 +211,7 @@ translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
 Lemma ap_refl [comp]:
   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
+  unfolding ap_def by compute
 
 Lemma (def) ap_pathcomp:
   assumes
@@ -224,7 +224,7 @@ Lemma (def) ap_pathcomp:
   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)
+      by (eq q) (compute, refl)
   qed
 
 Lemma (def) ap_pathinv:
@@ -234,7 +234,7 @@ Lemma (def) ap_pathinv:
     "f: A \<rightarrow> B"
     "p: x = y"
   shows "f[p\<inverse>] = f[p]\<inverse>"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) ap_funcomp:
   assumes
@@ -244,14 +244,14 @@ Lemma (def) ap_funcomp:
     "p: x = y"
   shows "(g \<circ> f)[p] = g[f[p]]"
   apply (eq p)
-  \<^item> by reduce
-  \<^item> by reduce refl
+  \<^item> by compute
+  \<^item> by compute refl
   done
 
 Lemma (def) ap_id:
   assumes "A: U i" "x: A" "y: A" "p: x = y"
   shows "(id A)[p] = p"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 
 section \<open>Transport\<close>
@@ -276,7 +276,7 @@ Lemma transport_comp [comp]:
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "transp P (refl a) \<equiv> id (P a)"
-  unfolding transport_def by reduce
+  unfolding transport_def by compute
 
 Lemma apply_transport:
   assumes
@@ -287,7 +287,7 @@ Lemma apply_transport:
   shows "transp P p\<inverse> u: P y"
   by typechk
 
-method transport uses eq = (rule apply_transport[OF _ _ _ _ eq])
+method rewr uses eq = (rule apply_transport[OF _ _ _ _ eq])
 
 Lemma (def) pathcomp_cancel_left:
   assumes
@@ -297,13 +297,13 @@ Lemma (def) pathcomp_cancel_left:
   shows "q = r"
   proof -
     have "q = (p\<inverse> \<bullet> p) \<bullet> q"
-      by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl
+      by (rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl
     also have ".. = p\<inverse> \<bullet> (p \<bullet> r)"
-      by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl
+      by (rewr eq: pathcomp_assoc[symmetric], rewr eq: \<open>\<alpha>:_\<close>) refl
     also have ".. = r"
-      by (transport eq: pathcomp_assoc,
-          transport eq: inv_pathcomp,
-          transport eq: refl_pathcomp) refl
+      by (rewr eq: pathcomp_assoc,
+          rewr eq: inv_pathcomp,
+          rewr eq: refl_pathcomp) refl
     finally show "?" by this
   qed
 
@@ -315,14 +315,14 @@ Lemma (def) pathcomp_cancel_right:
   shows "p = q"
   proof -
     have "p = p \<bullet> r \<bullet> r\<inverse>"
-      by (transport eq: pathcomp_assoc[symmetric],
-          transport eq: pathcomp_inv,
-          transport eq: pathcomp_refl) refl
+      by (rewr eq: pathcomp_assoc[symmetric],
+          rewr eq: pathcomp_inv,
+          rewr eq: pathcomp_refl) refl
     also have ".. = q"
-      by (transport eq: \<open>\<alpha>:_\<close>,
-          transport eq: pathcomp_assoc[symmetric],
-          transport eq: pathcomp_inv,
-          transport eq: pathcomp_refl) refl
+      by (rewr eq: \<open>\<alpha>:_\<close>,
+          rewr eq: pathcomp_assoc[symmetric],
+          rewr eq: pathcomp_inv,
+          rewr eq: pathcomp_refl) refl
     finally show "?" by this
   qed
 
@@ -336,7 +336,7 @@ Lemma (def) transport_left_inv:
     "x: A" "y: A"
     "p: x = y"
   shows "(transp P p\<inverse>) \<circ> (transp P p) = id (P x)"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) transport_right_inv:
   assumes
@@ -345,7 +345,7 @@ Lemma (def) transport_right_inv:
     "x: A" "y: A"
     "p: x = y"
   shows "(transp P p) \<circ> (transp P p\<inverse>) = id (P y)"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) transport_pathcomp:
   assumes
@@ -359,7 +359,7 @@ proof (eq p)
   fix x q u
   assuming "x: A" "q: x = z" "u: P x"
   show "transp P q (transp P (refl x) u) = transp P ((refl x) \<bullet> q) u"
-    by (eq q) (reduce, refl)
+    by (eq q) (compute, refl)
 qed
 
 Lemma (def) transport_compose_typefam:
@@ -371,7 +371,7 @@ Lemma (def) transport_compose_typefam:
     "p: x = y"
     "u: P (f x)"
   shows "transp (fn x. P (f x)) p u = transp P f[p] u"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) transport_function_family:
   assumes
@@ -383,7 +383,7 @@ Lemma (def) transport_function_family:
     "u: P x"
     "p: x = y"
   shows "transp Q p ((f x) u) = (f y) (transp P p u)"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 Lemma (def) transport_const:
   assumes
@@ -391,7 +391,7 @@ Lemma (def) transport_const:
     "x: A" "y: A"
     "p: x = y"
   shows "\<Prod>b: B. transp (fn _. B) p b = b"
-  by intro (eq p, reduce, refl)
+  by intro (eq p, compute, refl)
 
 definition transport_const_i ("transp'_c")
   where [implicit]: "transp_c B p \<equiv> transport_const {} B {} {} p"
@@ -403,7 +403,7 @@ Lemma transport_const_comp [comp]:
     "x: A" "b: B"
     "A: U i" "B: U i"
   shows "transp_c B (refl x) b \<equiv> refl b"
-  unfolding transport_const_def by reduce
+  unfolding transport_const_def by compute
 
 Lemma (def) pathlift:
   assumes
@@ -413,7 +413,7 @@ Lemma (def) pathlift:
     "p: x = y"
     "u: P x"
   shows "<x, u> = <y, transp P p u>"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 definition pathlift_i ("lift")
   where [implicit]: "lift P p u \<equiv> pathlift {} P {} {} p u"
@@ -427,7 +427,7 @@ Lemma pathlift_comp [comp]:
     "\<And>x. x: A \<Longrightarrow> P x: U i"
     "A: U i"
   shows "lift P (refl x) u \<equiv> refl <x, u>"
-  unfolding pathlift_def by reduce
+  unfolding pathlift_def by compute
 
 Lemma (def) pathlift_fst:
   assumes
@@ -437,7 +437,7 @@ Lemma (def) pathlift_fst:
     "u: P x"
     "p: x = y"
   shows "fst[lift P p u] = p"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 
 section \<open>Dependent paths\<close>
@@ -450,7 +450,7 @@ Lemma (def) apd:
     "x: A" "y: A"
     "p: x = y"
   shows "transp P p (f x) = f y"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 definition apd_i ("apd")
   where [implicit]: "apd f p \<equiv> Identity.apd {} {} f {} {} p"
@@ -464,7 +464,7 @@ Lemma dependent_map_comp [comp]:
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "apd f (refl x) \<equiv> refl (f x)"
-  unfolding apd_def by reduce
+  unfolding apd_def by compute
 
 Lemma (def) apd_ap:
   assumes
@@ -473,7 +473,7 @@ Lemma (def) apd_ap:
     "x: A" "y: A"
     "p: x = y"
   shows "apd f p = transp_c B p (f x) \<bullet> f[p]"
-  by (eq p) (reduce, refl)
+  by (eq p) (compute, refl)
 
 
 section \<open>Whiskering\<close>
@@ -519,12 +519,12 @@ translations
 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 (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
-  unfolding right_whisker_def by reduce
+  unfolding right_whisker_def by compute
 
 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 \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
-  unfolding left_whisker_def by reduce
+  unfolding left_whisker_def by compute
 
 method left_whisker = (rule left_whisker)
 method right_whisker = (rule right_whisker)
@@ -569,7 +569,7 @@ Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
   unfolding horiz_pathcomp_def horiz_pathcomp'_def
   apply (eq \<alpha>, eq \<beta>)
     focus vars p apply (eq p)
-      focus vars a _ _ _ r by (eq r) (reduce, refl)
+      focus vars a _ _ _ r by (eq r) (compute, refl)
     done
   done
 
@@ -604,14 +604,14 @@ Lemma
     and horiz_pathcomp'_type [type]: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
   using assms
   unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_def
-  by reduce+
+  by compute+
 
 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_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*)
-  proof (reduce, rule pathinv)
+  proof (compute, rule pathinv)
     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)
@@ -633,7 +633,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
   shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
   unfolding \<Omega>2.horiz_pathcomp'_def
   using assms[unfolded \<Omega>2_def, type]
-  proof reduce
+  proof compute
     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)
@@ -660,7 +660,7 @@ Lemma (def) eckmann_hilton:
     also have [simplified comp]: ".. = \<alpha> \<star>' \<beta>"
       \<comment> \<open>Danger! Inferred implicit has an equivalent form but needs to be
           manually simplified.\<close>
-      by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
+      by (rewr 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>"
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 1aa7932..33a5d0a 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -70,27 +70,27 @@ Lemma add_type [type]:
 Lemma add_zero [comp]:
   assumes "m: Nat"
   shows "m + 0 \<equiv> m"
-  unfolding add_def by reduce
+  unfolding add_def by compute
 
 Lemma add_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m + suc n \<equiv> suc (m + n)"
-  unfolding add_def by reduce
+  unfolding add_def by compute
 
 Lemma (def) zero_add:
   assumes "n: Nat"
   shows "0 + n = n"
   apply (elim n)
-    \<^item> by (reduce; intro)
-    \<^item> vars _ ih by reduce (eq ih; refl)
+    \<^item> by (compute; intro)
+    \<^item> vars _ ih by compute (eq ih; refl)
   done
 
 Lemma (def) suc_add:
   assumes "m: Nat" "n: Nat"
   shows "suc m + n = suc (m + n)"
   apply (elim n)
-    \<^item> by reduce refl
-    \<^item> vars _ ih by reduce (eq ih; refl)
+    \<^item> by compute refl
+    \<^item> vars _ ih by compute (eq ih; refl)
   done
 
 Lemma (def) suc_eq:
@@ -102,19 +102,19 @@ Lemma (def) add_assoc:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l + (m + n) = l + m+ n"
   apply (elim n)
-    \<^item> by reduce intro
-    \<^item> vars _ ih by reduce (eq ih; refl)
+    \<^item> by compute intro
+    \<^item> vars _ ih by compute (eq ih; refl)
   done
 
 Lemma (def) add_comm:
   assumes "m: Nat" "n: Nat"
   shows "m + n = n + m"
   apply (elim n)
-    \<^item> by (reduce; rule zero_add[symmetric])
+    \<^item> by (compute; rule zero_add[symmetric])
     \<^item> vars n ih
-      proof reduce
+      proof compute
         have "suc (m + n) = suc (n + m)" by (eq ih) refl
-        also have ".. = suc n + m" by (transport eq: suc_add) refl
+        also have ".. = suc n + m" by (rewr eq: suc_add) refl
         finally show "?" by this
       qed
   done
@@ -131,27 +131,27 @@ Lemma mul_type [type]:
 Lemma mul_zero [comp]:
   assumes "n: Nat"
   shows "n * 0 \<equiv> 0"
-  unfolding mul_def by reduce
+  unfolding mul_def by compute
 
 Lemma mul_one [comp]:
   assumes "n: Nat"
   shows "n * 1 \<equiv> n"
-  unfolding mul_def by reduce
+  unfolding mul_def by compute
 
 Lemma mul_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m * suc n \<equiv> m + m * n"
-  unfolding mul_def by reduce
+  unfolding mul_def by compute
 
 Lemma (def) zero_mul:
   assumes "n: Nat"
   shows "0 * n = 0"
   apply (elim n)
-  \<^item> by reduce refl
+  \<^item> by compute refl
   \<^item> vars n ih
-    proof reduce
+    proof compute
       have "0 + 0 * n = 0 + 0 " by (eq ih) refl
-      also have ".. = 0" by reduce refl
+      also have ".. = 0" by compute refl
       finally show "?" by this
     qed
   done
@@ -160,11 +160,11 @@ Lemma (def) suc_mul:
   assumes "m: Nat" "n: Nat"
   shows "suc m * n = m * n + n"
   apply (elim n)
-  \<^item> by reduce refl
+  \<^item> by compute refl
   \<^item> vars n ih
-    proof (reduce, transport eq: \<open>ih:_\<close>)
+    proof (compute, rewr 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
+      also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl
       finally show "?" by this
     qed
   done
@@ -173,13 +173,13 @@ Lemma (def) mul_dist_add:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l * (m + n) = l * m + l * n"
   apply (elim n)
-  \<^item> by reduce refl
+  \<^item> by compute refl
   \<^item> vars n ih
-    proof reduce
+    proof compute
       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)
-      also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl
-      also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl
+      also have ".. = l * m + l + l * n" by (rewr eq: add_comm) refl
+      also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl
       finally show "?" by this
     qed
   done
@@ -188,11 +188,11 @@ Lemma (def) mul_assoc:
   assumes "l: Nat" "m: Nat" "n: Nat"
   shows "l * (m * n) = l * m * n"
   apply (elim n)
-  \<^item> by reduce refl
+  \<^item> by compute refl
   \<^item> vars n ih
-    proof reduce
+    proof compute
       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
+      also have ".. = l * m + l * m * n" by (rewr eq: \<open>ih:_\<close>) refl
       finally show "?" by this
     qed
   done
@@ -201,12 +201,12 @@ Lemma (def) mul_comm:
   assumes "m: Nat" "n: Nat"
   shows "m * n = n * m"
   apply (elim n)
-  \<^item> by reduce (transport eq: zero_mul, refl)
+  \<^item> by compute (rewr eq: zero_mul, refl)
   \<^item> vars n ih
-    proof (reduce, rule pathinv)
+    proof (compute, rule pathinv)
       have "suc n * m = n * m + m" by (rule suc_mul)
       also have ".. = m + m * n"
-        by (transport eq: \<open>ih:_\<close>, transport eq: add_comm) refl
+        by (rewr eq: \<open>ih:_\<close>, rewr eq: add_comm) refl
       finally show "?" by this
     qed
   done
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ffe3778..5046b6a 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -295,7 +295,7 @@ method_setup this =
 
 subsection \<open>Rewriting\<close>
 
-consts rewrite_hole :: "'a::{}"  ("\<hole>")
+consts compute_hole :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
@@ -319,10 +319,10 @@ lemma imp_cong_eq:
   done
 
 ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
-ML_file \<open>rewrite.ML\<close>
+ML_file \<open>comp.ML\<close>
 
-\<comment> \<open>\<open>reduce\<close> simplifies terms via computational equalities\<close>
-method reduce uses add =
+\<comment> \<open>\<open>compute\<close> simplifies terms via computational equalities\<close>
+method compute uses add =
   changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
 
 
@@ -396,7 +396,7 @@ Lemma refine_codomain:
     "f: \<Prod>x: A. B x"
     "\<And>x. x: A \<Longrightarrow> f `x: C x"
   shows "f: \<Prod>x: A. C x"
-  by (rewrite eta_exp)
+  by (comp eta_exp)
 
 Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
@@ -432,7 +432,7 @@ Lemma funcomp_assoc [comp]:
     "h: \<Prod>x: C. D x"
   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
+  unfolding funcomp_def by compute
 
 Lemma funcomp_lambda_comp [comp]:
   assumes
@@ -441,7 +441,7 @@ Lemma funcomp_lambda_comp [comp]:
     "\<And>x. x: B \<Longrightarrow> c x: C x"
   shows
     "(\<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
+  unfolding funcomp_def by compute
 
 Lemma funcomp_apply_comp [comp]:
   assumes
@@ -449,7 +449,7 @@ Lemma funcomp_apply_comp [comp]:
     "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
     "x: A"
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
-  unfolding funcomp_def by reduce
+  unfolding funcomp_def by compute
 
 subsection \<open>Notation\<close>
 
@@ -465,17 +465,17 @@ abbreviation id where "id A \<equiv> \<lambda>x: A. x"
 lemma
   id_type [type]: "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+
+  by compute+
 
 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 (rewrite eta_exp[of f]) (reduce, rule eta)
+  by (comp eta_exp[of f]) (compute, rule eta)
 
 Lemma id_right [comp]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
-  by (rewrite eta_exp[of f]) (reduce, rule eta)
+  by (comp eta_exp[of f]) (compute, rule eta)
 
 lemma id_U [type]:
   "id (U i): U i \<rightarrow> U i"
@@ -496,7 +496,7 @@ 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
+  unfolding fst_def by compute
 
 Lemma snd_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
@@ -506,7 +506,7 @@ Lemma snd_type [type]:
 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
+  unfolding snd_def by compute
 
 subsection \<open>Notation\<close>
 
diff --git a/spartan/core/rewrite.ML b/spartan/core/comp.ML
index af70cfc..2e50753 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/comp.ML
@@ -1,10 +1,16 @@
-(*  Title:      rewrite.ML
+(*  Title:      compute.ML
     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     Modified:   Joshua Chen, University of Innsbruck
 
-This is a rewrite method that supports subterm-selection based on patterns.
+This is a method for rewriting computational equalities that supports subterm
+selection based on patterns.
 
-The patterns accepted by rewrite are of the following form:
+This code has been slightly modified from the original at HOL/Library/compute.ML
+to incorporate automatic discharge of type-theoretic side conditions.
+
+Comment from the original code follows:
+
+The patterns accepted by compute are of the following form:
   <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
   <pattern> ::= (in <atom> | at <atom>) [<pattern>]
   <args>    ::= [<pattern>] ("to" <term>) <thms>
@@ -14,15 +20,12 @@ patterns but has diverged significantly during its development.
 
 We also allow introduction of identifiers for bound variables,
 which can then be used to match arbitrary subterms inside abstractions.
-
-This code has been slightly modified from the original at HOL/Library/rewrite.ML
-to incorporate automatic discharge of type-theoretic side conditions.
 *)
 
 infix 1 then_pconv;
 infix 0 else_pconv;
 
-signature REWRITE =
+signature COMPUTE =
 sig
   type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv
   val then_pconv: patconv * patconv -> patconv
@@ -41,19 +44,19 @@ sig
   val judgment_pconv: patconv -> patconv
   val in_pconv: patconv -> patconv
   val match_pconv: patconv -> term * (string option * typ) list -> patconv
-  val rewrs_pconv: term option -> thm list -> patconv
+  val comps_pconv: term option -> thm list -> patconv
 
   datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
 
   val mk_hole: int -> typ -> term
 
-  val rewrite_conv: Proof.context
+  val compute_conv: Proof.context
     -> (term * (string * typ) list, string * typ option) pattern list * term option
     -> thm list
     -> conv
 end
 
-structure Rewrite : REWRITE =
+structure Compute : COMPUTE =
 struct
 
 datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
@@ -72,13 +75,13 @@ fun mk_hole i T = Var ((holeN, i), T)
 fun is_hole (Var ((name, _), _)) = (name = holeN)
   | is_hole _ = false
 
-fun is_hole_const (Const (\<^const_name>\<open>rewrite_hole\<close>, _)) = true
+fun is_hole_const (Const (\<^const_name>\<open>compute_hole\<close>, _)) = true
   | is_hole_const _ = false
 
 val hole_syntax =
   let
     (* Modified variant of Term.replace_hole *)
-    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_hole\<close>, T)) i =
+    fun replace_hole Ts (Const (\<^const_name>\<open>compute_hole\<close>, T)) i =
           (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
       | replace_hole Ts (Abs (x, T, t)) i =
           let val (t', i') = replace_hole (T :: Ts) t i
@@ -265,7 +268,7 @@ fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct =
     | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct
   end
 
-fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
+fun comps_pconv to thms ctxt (tyenv, env_ts) =
   let
     fun instantiate_normalize_env ctxt env thm =
       let
@@ -301,7 +304,7 @@ fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
     
   in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
 
-fun rewrite_conv ctxt (pattern, to) thms ct =
+fun compute_conv ctxt (pattern, to) thms ct =
   let
     fun apply_pat At = judgment_pconv
       | apply_pat In = in_pconv
@@ -317,15 +320,15 @@ fun rewrite_conv ctxt (pattern, to) thms ct =
         NONE => th
       | SOME (th', _) => th'
 
-    val rewrite = rewrs_pconv to (maps (prep_meta_eq ctxt) thms)
-  in cv rewrite ctxt (Vartab.empty, []) ct |> distinct_prems end
+    val compute = comps_pconv to (maps (prep_meta_eq ctxt) thms)
+  in cv compute ctxt (Vartab.empty, []) ct |> distinct_prems end
 
-fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
+fun compute_export_tac ctxt (pat, pat_ctxt) thms =
   let
     val export = case pat_ctxt of
         NONE => I
       | SOME inner => singleton (Proof_Context.export inner ctxt)
-  in CCONVERSION (export o rewrite_conv ctxt pat thms) end
+  in CCONVERSION (export o compute_conv ctxt pat thms) end
 
 val _ =
   Theory.setup
@@ -449,17 +452,17 @@ val _ =
       let val scan = raw_pattern -- to_parser -- Parse.thms1
       in context_lift scan prep_args end
 
-    fun rewrite_export_ctac inputs inthms =
-      CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms)
+    fun compute_export_ctac inputs inthms =
+      CONTEXT_TACTIC' (fn ctxt => compute_export_tac ctxt inputs inthms)
   in
-    Method.setup \<^binding>\<open>rewr\<close> (subst_parser >>
+    Method.setup \<^binding>\<open>cmp\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD'
-        (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
+        (compute_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
       "single-step rewriting, allowing subterm selection via patterns" #>
-    Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
+    Method.setup \<^binding>\<open>comp\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD (
         CHEADGOAL o SIDE_CONDS 0
-          (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
+          (compute_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
       "single-step rewriting with auto-typechecking"
   end
 end
diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML
index c372ca7..5aa7c70 100644
--- a/spartan/core/context_facts.ML
+++ b/spartan/core/context_facts.ML
@@ -17,6 +17,7 @@ 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
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 1501221..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -114,7 +114,7 @@ Lemma head_type [type]:
 Lemma head_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "head (x # xs) \<equiv> some x"
-  unfolding head_def by reduce
+  unfolding head_def by compute
 
 Lemma tail_type [type]:
   assumes "A: U i" "xs: List A"
@@ -124,7 +124,7 @@ Lemma tail_type [type]:
 Lemma tail_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "tail (x # xs) \<equiv> xs"
-  unfolding tail_def by reduce
+  unfolding tail_def by compute
 
 subsection \<open>Append\<close>
 
@@ -185,7 +185,7 @@ Lemma rev_type [type]:
 Lemma rev_nil [comp]:
   assumes "A: U i"
   shows "rev (nil A) \<equiv> nil A"
-  unfolding rev_def by reduce
+  unfolding rev_def by compute
 
 
 end
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index e06a07b..452acc2 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -40,7 +40,7 @@ Lemma Maybe_comp_none:
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 Lemma Maybe_comp_some:
   assumes
@@ -52,7 +52,7 @@ Lemma Maybe_comp_some:
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 0043c1e..56adbfc 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -116,7 +116,7 @@ Lemma if_true:
   shows "ifelse C true a b \<equiv> a"
   unfolding ifelse_def true_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 Lemma if_false:
   assumes
@@ -126,7 +126,7 @@ Lemma if_false:
   shows "ifelse C false a b \<equiv> b"
   unfolding ifelse_def false_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 lemmas
   [form] = BoolF and
@@ -145,7 +145,7 @@ translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
 
 subsection \<open>Logical connectives\<close>
 
-definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
+definition not ("!_") where "!x \<equiv> ifelse (K Bool) x false true"
 
 
 end