Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!

15 files changed, 177 insertions, 273 deletions

diff --git a/Coprod.thy b/Coprod.thy
index d97228e..431e103 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -42,6 +42,7 @@ where
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
     \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b"
 
+lemmas Coprod_form [form]
 lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim
 lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr
 
diff --git a/Empty.thy b/Empty.thy
index 3060867..ee11045 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -20,6 +20,7 @@ where
 
   Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
 
+lemmas Empty_form [form]
 lemmas Empty_routine [intro] = Empty_form Empty_elim
 
 
diff --git a/Equal.thy b/Equal.thy
index 7a31e37..19e3939 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -44,6 +44,7 @@ axiomatization where
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
     \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
+lemmas Equal_form [form]
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]
 
diff --git a/HoTT.thy b/HoTT.thy
index e2a7e35..0e7a674 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,5 +1,7 @@
-(*  Title:  HoTT/HoTT.thy
-    Author: Josh Chen
+(*
+Title:  HoTT.thy
+Author: Joshua Chen
+Date:   2018
 
 Homotopy type theory
 *)
@@ -26,8 +28,7 @@ Proj
 begin
 
 
-lemmas forms =
-  Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+text \<open>Rule bundles:\<close>
 
 lemmas intros =
   Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 7453883..2ad0ac5 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,7 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty
 *)
 
 theory HoTT_Base
-imports Pure "HOL-Eisbach.Eisbach"
+imports Pure
 
 begin
 
@@ -18,17 +18,14 @@ typedecl t  \<comment> \<open>Type of object types and terms\<close>
 typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
 axiomatization
-  O :: ord and
+  O   :: ord and
   Suc :: "ord \<Rightarrow> ord" and
-  lt :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999)
+  lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
+  leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 999)
 where
   lt_Suc [intro]: "n < (Suc n)" and
   lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
-  Suc_monotone [simp]: "m < n \<Longrightarrow> (Suc m) < (Suc n)"
-
-method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
-
-text \<open>Method @{method proveSuc} proves statements of the form \<open>n < (Suc (... (Suc n) ...))\<close>.\<close>
+  leq_min [intro]: "O \<le> n"
 
 
 section \<open>Judgment\<close>
@@ -42,15 +39,15 @@ axiomatization
   U :: "ord \<Rightarrow> t"
 where
   U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
-  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j"
+  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
+  U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
 Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
 One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
-\<close>
 
-method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>\<close>
-method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...))\<close>\<close>
+@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+\<close>
 
 
 section \<open>Type families\<close>
@@ -68,11 +65,15 @@ type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<
 section \<open>Named theorems\<close>
 
 named_theorems comp
+named_theorems form
 
 text \<open>
 Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
-@{attribute comp} declares computation rules.
-These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute form} declares type formation rules.
+These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
 \<close>
 
 (* Todo: Set up the Simplifier! *)
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 8929f69..f0cee6c 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -12,6 +12,26 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 begin
 
 
+section \<open>Handling universes\<close>
+
+method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
+
+method hierarchy = (rule U_hierarchy, provelt)
+
+method cumulativity declares form = (
+  ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) |
+  ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
+)
+
+text \<open>
+Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form
+\<^item> \<open>n < (Suc (... (Suc n) ...))\<close>,
+\<^item> \<open>U i: U (Suc (... (Suc i) ...))\<close>, and
+\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"}
+respectively.
+\<close>
+
+
 section \<open>Deriving typing judgments\<close>
 
 method routine uses add = (assumption | rule add | rule)+
@@ -38,14 +58,15 @@ Method @{method compute} performs single-step simplifications, using any rules d
 Premises of the rule(s) applied are added as new subgoals.
 \<close>
 
+
 section \<open>Derivation search\<close>
 
 text \<open>
 Combine @{method routine} and @{method compute} to search for derivations of judgments.
-Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}.
+Also handle universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+
+method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
 
 section \<open>Induction\<close>
diff --git a/Nat.thy b/Nat.thy
index 46b1af5..8a55852 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -41,6 +41,7 @@ where
     C: \<nat> \<longrightarrow> U i;
     \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
+lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
 lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
 
diff --git a/Prod.thy b/Prod.thy
index 4aa7119..f90ee9c 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -61,6 +61,7 @@ Note that this is a separate rule from function extensionality.
 Note that the bold lambda symbol \<open>\<^bold>\<lambda>\<close> used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation).
 \<close>
 
+lemmas Prod_form [form]
 lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
diff --git a/Sum.thy b/Sum.thy
index 422e01b..463a9d4 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -51,6 +51,7 @@ axiomatization where
 
   Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x"
 
+lemmas Sum_form [form]
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
 lemmas Sum_comp [comp]
 
diff --git a/Unit.thy b/Unit.thy
index 61c6439..7c221f0 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -25,6 +25,7 @@ where
 
   Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
 
+lemmas Unit_form [form]
 lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
 lemmas Unit_comp [comp]
 
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index a577fca..263f43d 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -1,55 +1,50 @@
-(*  Title:  HoTT/ex/HoTT book/Ch1.thy
-    Author: Josh Chen
+(*
+Title:  ex/HoTT book/Ch1.thy
+Author: Josh Chen
+Date:   2018
 
 A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
 *)
 
 theory Ch1
-  imports "../../HoTT"
+imports "../../HoTT"
+
 begin
 
 chapter \<open>HoTT Book, Chapter 1\<close>
 
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
 
-text "Propositional uniqueness principle:"
+paragraph \<open>Propositional uniqueness principle.\<close>
 
 schematic_goal
-  assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
-  shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x"
+  shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>"
 
-text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
+text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
 
 proof (rule Sum_elim[where ?p=p])
-  text "We just need to prove the base case; the rest will be taken care of automatically."
-
-  fix x y assume asm: "x: A" "y: B(x)" show
-    "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
-  proof (subst (0 1) comp)
-    text "
-      The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types.
-      The automatic proof methods have trouble picking the appropriate types, so we state them explicitly,
-    "
-    show "x: A" and "y: B(x)" by (fact asm)+
-
-    text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>."
-    show "x: A" and "y: B(x)" by (fact asm)+
+  text \<open>We prove the base case.\<close>
+  fix x y assume asm: "x: A" "y: B x" show "refl <x,y>: <x,y> =[\<Sum>x:A. B x] <fst <x,y>, snd <x,y>>"
+  proof compute
+    show "x: A" and "y: B x" by (fact asm)+  \<comment> \<open>Hint the correct types.\<close>
 
+    text \<open>And now @{method derive} takes care of the rest.
+\<close>
   qed (derive lems: assms asm)
-
 qed (derive lems: assms)
 
 
 section \<open>Exercises\<close>
 
-text "Exercise 1.13"
+paragraph \<open>Exercise 1.13\<close>
 
-abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>"
+abbreviation "not" ("\<not>_") where "\<not>A \<equiv> A \<rightarrow> \<zero>"
 
 text "This proof requires the use of universe cumulativity."
 
-proposition assumes "A: U(i)" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`inl(a))): \<not>(\<not>(A + \<not>(A)))"
-by (derive lems: assms U_cumulative[where ?A=\<zero> and ?i=O and ?j=i])
+proposition assumes "A: U i" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`(inl a))): \<not>(\<not>(A + \<not>A))"
+by (derive lems: assms)
 
 
 end
diff --git a/ex/Methods.thy b/ex/Methods.thy
index c78af14..09975b0 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -1,76 +1,49 @@
-(*  Title:  HoTT/ex/Methods.thy
-    Author: Josh Chen
+(*
+Title:  ex/Methods.thy
+Author: Joshua Chen
+Date:   2018
 
-HoTT method usage examples
+Basic HoTT method usage examples.
 *)
 
 theory Methods
-  imports "../HoTT"
-begin
+imports "../HoTT"
 
+begin
 
-text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules."
 
 lemma
   assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)"
-  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)"
-by (routine lems: assms)
-
-
-lemma
-  assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)"
-  shows
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-proof -
-  show
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-  by (derive lems: assms)
-qed
-
-
-text "Typechecking and constructing inhabitants:"
+  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w: U(i)"
+by (routine add: assms)
 
-\<comment> \<open>Correctly determines the type of the pair\<close>
+\<comment> \<open>Correctly determines the type of the pair.\<close>
 schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A"
 by routine
 
 \<comment> \<open>Finds pair (too easy).\<close>
 schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B"
-apply (rule Sum_intro)
+apply (rule intros)
 apply assumption+
 done
 
-
-text "
-  Function application.
-  The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types.
-"
-
-lemma
-  assumes "A: U(i)" "a: A"
-  shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
+\<comment> \<open>Function application. We still often have to explicitly specify types.\<close>
+lemma "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
 proof compute
   show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine
-qed (routine lems: assms)
-
+qed
 
-lemma
-  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)"
-  shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
-proof compute
-  show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms)
+text \<open>
+The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof.
+\<close>
 
-  show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>"
+lemma "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
+proof (compute, routine)
+  show "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>y. <a,y>)`b \<equiv> <a,b>"
   proof compute
-    show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms)
-  qed fact
-qed fact
+    show "\<And>b. \<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" by routine
+  qed
+qed
 
 
 end
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index a5e77ec..3ee973c 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -1,78 +1,58 @@
-(*  Title:  HoTT/ex/Synthesis.thy
-    Author: Josh Chen
+(*
+Title:  ex/Synthesis.thy
+Author: Joshua Chen
+Date:   2018
 
-Examples of synthesis.
+Examples of synthesis
 *)
 
 
 theory Synthesis
-  imports "../HoTT"
+imports "../HoTT"
+
 begin
 
 
 section \<open>Synthesis of the predecessor function\<close>
 
-text "
-  In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers.
-
-  This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely.
-"
+text \<open>
+In this example we construct a predecessor function for the natural numbers.
+This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional.
+\<close>
 
-text "First we show that the property we want is well-defined."
+text \<open>First we show that the property we want is well-defined.\<close>
 
-lemma pred_welltyped: "\<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n): U(O)"
+lemma pred_welltyped: "\<Sum>pred: \<nat>\<rightarrow>\<nat>. (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n): U O"
 by routine
 
-text "
-  Now we look for an inhabitant of this type.
-  Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>.
-  What if we require **definitional** equality instead of just propositional equality?
-"
+text \<open>
+Now we look for an inhabitant of this type.
+Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\<nat> 0"} and @{term "\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n"}.
+What if we require *definitional* instead of just propositional equality?
+\<close>
 
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
 apply compute
 prefer 4 apply compute
-prefer 3 apply compute
-apply (rule Nat_routine Nat_elim | compute | assumption)+
-done
-
-text "
-  The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n\<close>.
-  We prove this has the required type and properties.
-"
-
-definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"
-
-lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by routine
-
-lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-proof (routine lems: pred_type)
-  have *: "pred`0 \<equiv> 0" unfolding pred_def
-  proof compute
-    show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
-    show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
-    proof compute
-      show "\<nat>: U(O)" ..
-    qed routine
-  qed rule
-  then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) routine
-
-  show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n"
-  unfolding pred_def proof
-    show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n"
-    proof compute
-      show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
-      show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n"
-      proof compute
-        show "\<nat>: U(O)" ..
-      qed routine
-    qed rule
-  qed rule
-qed
-
-theorem
-  "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-by (routine lems: pred_welltyped pred_type pred_props)
+apply (rule Nat_routine | compute)+
+oops
+\<comment> \<open>Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\<close>
+
+text \<open>
+The above proof finds a candidate, namely @{term "\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"}.
+We prove this has the required type and properties.
+\<close>
+
+definition pred :: t where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"
+
+lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>"
+unfolding pred_def by routine
+
+lemma pred_props: "<refl 0, \<^bold>\<lambda>n. refl n>: (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n)"
+unfolding pred_def by derive
+
+theorem "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
+by (derive lems: pred_type pred_props)
 
 
 end
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy
deleted file mode 100644
index 82d7e5d..0000000
--- a/tests/Subgoal.thy
+++ /dev/null
@@ -1,63 +0,0 @@
-theory Subgoal
-  imports "../HoTT"
-begin
-
-
-text "
-  Proof of \<open>rpathcomp_type\<close> (see EqualProps.thy) in apply-style.
-  Subgoaling can be used to fix variables and apply the elimination rules.
-"
-
-lemma rpathcomp_type:
-  assumes "A: U(i)"
-  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding rpathcomp_def
-apply standard
-  subgoal premises 1 for x  \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close>
-  apply standard
-    subgoal premises 2 for y
-    apply standard
-      subgoal premises 3 for p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-        \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close>
-      prefer 4
-        apply standard
-          apply (rule Prod_intro)
-            subgoal premises 4 for u z q
-            apply (rule Equal_elim[where ?x=u and ?y=z])
-            apply (routine lems: assms 4)
-            done
-          apply (routine lems: assms 1 2 3)
-      done
-    apply (routine lems: assms 1 2)
-    done
-  apply fact
-  done
-apply fact
-done
-
-
-text "
-  \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs.
-  This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof.
-
-  This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact.
-"
-
-schematic_goal rpathcomp_synthesis:
-  assumes "A: U(i)"
-  shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-
-text "
-  Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below.
-"
-
-apply (rule intros)
-  apply (rule intros)
-    apply (rule intros)
-      subgoal 123 for x y p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-      oops
-
-
-end
diff --git a/tests/Test.thy b/tests/Test.thy
index de65dbd..6f9f996 100644
--- a/tests/Test.thy
+++ b/tests/Test.thy
@@ -1,121 +1,110 @@
-(*  Title:  HoTT/tests/Test.thy
-    Author: Josh Chen
-    Date:   Aug 2018
+(*
+Title:  tests/Test.thy
+Author: Joshua Chen
+Date:   2018
 
-This is an old "test suite" from early implementations of the theory.
-It is not always guaranteed to be up to date, or reflect most recent versions of the theory.
+This is an old test suite from early implementations.
+It is not always guaranteed to be up to date or to reflect most recent versions of the theory.
 *)
 
 theory Test
-  imports "../HoTT"
+imports "../HoTT"
+
 begin
 
 
-text "
-  A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
-  
-  Things that *should* be automated:
-    - Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
-    - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
-"
+text \<open>
+A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
+
+Things that *should* be automated:
+\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}.
+\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
+\<close>
 
 declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
-  \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
+\<comment> \<open>Turn on trace for unification and the Simplifier, for debugging.\<close>
 
 
 section \<open>\<Prod>-type\<close>
 
 subsection \<open>Typing functions\<close>
 
-text "
-  Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
-"
+text \<open>Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\<close>
 
-proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (routine lems: assms)
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A"
+by (routine add: assms)
 
 proposition
   assumes "A : U(i)" and "A \<equiv> B"
   shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
 proof -
   have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp
-  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine lems: assms)
+  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine add: assms)
   ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
 qed
 
 proposition
   assumes "A : U(i)" and "B : U(i)"
   shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
-by (routine lems: assms)
-
+by (routine add: assms)
 
 subsection \<open>Function application\<close>
 
-proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (derive lems: assms)
-
-text "Currying:"
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a"
+by (derive lems: assms)
 
 lemma
   assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
   shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
-proof compute
-  show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (routine lems: assms)
-qed fact
+by (derive lems: assms)
 
-lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by derive
+lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b"
+by derive
 
-lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
-proof compute
-  show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y"
-  proof
-    oops
+lemma "\<lbrakk>A: U(i); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
+proof derive
+oops  \<comment> \<open>Missing some premises.\<close>
 
 lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c"
-  oops
+proof derive
+oops
 
 
 subsection \<open>Currying functions\<close>
 
 proposition curried_function_formation:
-  fixes A B C
-  assumes
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
+  assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
   shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)"
-  by (routine lems: assms)
-
+by (routine add: assms)
 
 proposition higher_order_currying_formation:
   assumes
-    "A: U(i)" and
-    "B: A \<longrightarrow> U(i)" and
+    "A: U(i)" and "B: A \<longrightarrow> U(i)" and
     "\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and
     "\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)"
   shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)"
-  by (routine lems: assms)
-
+by (routine add: assms)
 
 lemma curried_type_judgment:
-  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
+  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
   shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
-  by (routine lems: assms)
+by (routine add: assms)
 
 
-text "
-  Polymorphic identity function is now trivial due to lambda expression polymorphism.
-  (Was more involved in previous monomorphic incarnations.)
-"
+text \<open>
+Polymorphic identity function is now trivial due to lambda expression polymorphism.
+It was more involved in previous monomorphic incarnations.
+\<close>
 
-definition Id :: "Term" where "Id \<equiv> \<^bold>\<lambda>x. x"
-
-lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x"
-unfolding Id_def by (compute, routine)
+lemma "x: A \<Longrightarrow> id`x \<equiv> x"
+by derive
   
 
 section \<open>Natural numbers\<close>
 
-text "Automatic proof methods recognize natural numbers."
+text \<open>Automatic proof methods recognize natural numbers.\<close>
+
+proposition "succ(succ(succ 0)): \<nat>" by routine
 
-proposition "succ(succ(succ 0)): Nat" by routine
 
 end