1 files changed, 23 insertions, 50 deletions
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