Equality inverse and composition done. Cleaned up methods and method example theory.

5 files changed, 215 insertions, 121 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index d645fb6..3d99456 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -1,6 +1,6 @@
 (*  Title:  HoTT/EqualProps.thy
     Author: Josh Chen
-    Date:   Jun 2018
+    Date:   Aug 2018
 
 Properties of equality.
 *)
@@ -18,22 +18,28 @@ section \<open>Symmetry / Path inverse\<close>
 axiomatization inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000)
   where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p"
 
+text "
+  In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use.
+  The proof is finished with a standard application of the relevant type rules.
+"
 
 lemma inv_type:
   assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
 unfolding inv_def
-proof (rule Equal_elim[where ?x=x and ?y=y])  \<comment> \<open>Path induction\<close>
-  show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) ..
-  show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-qed (fact assms)+
+by (rule Equal_elim[where ?x=x and ?y=y]) (simple lem: assms)
+  \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close>
 
+text "
+  The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules.
+  (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.)
+"
 
-lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
+lemma inv_comp:
+  assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
 unfolding inv_def
 proof
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-  show "\<And>x. x: A \<Longrightarrow> x =\<^sub>A x: U(i)" using assms(1) ..
-qed (fact assms)
+qed (simple lem: assms)
 
 
 section \<open>Transitivity / Path composition\<close>
@@ -45,67 +51,173 @@ text "
 axiomatization rcompose :: Term where
   rcompose_def: "rcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
 
+text "
+  More complicated proofs---the nested path inductions require more explicit step-by-step rule applications:
+"
 
 lemma rcompose_type:
   assumes "A: U(i)"
   shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
 unfolding rcompose_def
 proof
-  show "\<And>x. x: A \<Longrightarrow>
-    \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+  fix x assume 1: "x: A"
+  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
   proof
-    show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow>
-       \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+    fix y assume 2: "y: A"
+    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
     proof
-      { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z"
+      fix p assume 3: "p: x =\<^sub>A y"
+      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
       proof (rule Equal_elim[where ?x=x and ?y=y])
-        show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
+        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
         proof
-          show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
-            by (rule Prod_form Equal_form assms | assumption)+
-        qed (rule assms)
-
-        show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-        proof
-          show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
           proof
-            { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z"
-            show "ind\<^sub>= refl p: x =[A] z"
-            proof (rule Equal_elim[where ?x=x and ?y=z])
-              show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
-              show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-            qed (fact asm)+ }
-            show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms)
-          qed
+            fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z"
+            show "ind\<^sub>= refl q: u =\<^sub>A z"
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm)
+          qed (simple lem: assms)
         qed (rule assms)
-      qed (rule asm)+ }
-      show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
-    qed
+      qed (simple lem: assms 1 2 3)
+    qed (simple lem: assms 1 2)
   qed (rule assms)
-qed (fact assms)
+qed fact
 
 corollary
   assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows "rcompose`x`y`p`z`q: x =\<^sub>A z"
-  by standard+ (rule rcompose_type assms)+
+  by (simple lem: assms rcompose_type)
 
+text "
+  The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule.
+"
+
+lemma rcompose_comp:
+  assumes "A: U(i)" and "a: A"
+  shows "rcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)"
+unfolding rcompose_def
+proof (subst comp)
+  { fix x assume 1: "x: A"
+  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+  proof
+    fix y assume 2: "y: A"
+    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+    proof
+      fix p assume 3: "p: x =\<^sub>A y"
+      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+      proof (rule Equal_elim[where ?x=x and ?y=y])
+        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
+        proof
+          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
+          proof
+            fix u z assume asm: "u: A" "z: A"
+            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm)
+          qed (simple lem: assms)
+        qed (rule assms)
+      qed (simple lem: assms 1 2 3)
+    qed (simple lem: assms 1 2)
+  qed (rule assms) }
+
+  show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)"
+  proof (subst comp)
+    { fix y assume 1: "y: A"
+    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)"
+      proof
+        fix p assume 2: "p: a =\<^sub>A y"
+        show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z"
+        proof (rule Equal_elim[where ?x=a and ?y=y])
+          fix u assume 3: "u: A"
+          show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =[A] z \<rightarrow> u =[A] z"
+          proof
+            fix z assume 4: "z: A"
+            show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
+            proof
+              show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
+              by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 3 4)
+            qed (simple lem: assms 3 4)
+          qed fact
+        qed (simple lem: assms 1 2)
+      qed (simple lem: assms 1) }
+    
+    show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)"
+    proof (subst comp)
+      { fix p assume 1: "p: a =\<^sub>A a"
+      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A a \<rightarrow> a =\<^sub>A z"
+      proof (rule Equal_elim[where ?x=a and ?y=a])
+        fix u assume 2: "u: A"
+        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z"
+        proof
+          fix z assume 3: "z: A"
+          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z"
+          proof
+            show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 2 3)
+          qed (simple lem: assms 2)
+        qed fact
+      qed (simple lem: assms 1) }
+      
+      show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)"
+      proof (subst comp)
+        { fix u assume 1: "u: A"
+        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z"
+        proof
+          fix z assume 2: "z: A"
+          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z"
+          proof
+            show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 1 2)
+          qed (simple lem: assms 1)
+        qed fact }
+        
+        show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)"
+        proof (subst comp)
+          { fix a assume 1: "a: A"
+          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
+          proof
+            show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a"
+            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms 1)
+          qed (simple lem: assms 1) }
+          
+          show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)"
+          proof (subst comp)
+            show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
+            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms)
+            show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)"
+            proof
+              show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" ..
+            qed (simple lem: assms)
+          qed (simple lem: assms)
+        qed fact
+      qed (simple lem: assms)
+    qed (simple lem: assms)
+  qed fact
+qed fact
+
+
+text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
 
 axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
-  compose_comp: "\<lbrakk>
+  compose_def: "\<lbrakk>
     A: U(i);
     x: A; y: A; z: A;
     p: x =\<^sub>A y; q: y =\<^sub>A z
   \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rcompose`x`y`p`z`q"
 
 
+lemma compose_type:
+  assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  shows "p \<bullet> q: x =\<^sub>A z"
+proof (subst compose_def)
+  show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
+qed (simple lem: assms rcompose_type)
+
 lemma compose_comp:
-  assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
-  unfolding rcompose_def
-  by (simplify lems: assms)
+  assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)"
+by (subst compose_def) (simple lem: assms rcompose_comp)
 
 
-lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp
+lemmas EqualProps_rules [intro] = inv_type compose_type
 lemmas EqualProps_comps [comp] = inv_comp compose_comp
 
 
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index f80b99b..e2eb4f1 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -13,69 +13,52 @@ theory HoTT_Methods
 begin
 
 
-section \<open>Setup\<close>
-
-text "Import the \<open>subst\<close> method, used by \<open>simplify\<close>."
-
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/eqsubst.ML"
-
-
 section \<open>Method definitions\<close>
 
 subsection \<open>Simple type rule proof search\<close>
 
-text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas.
-
-Can also perform typechecking, and search for elements of a type."
+text "
+  Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas.
+  
+  Can also perform typechecking, and search for elements of a type.
+"
 
-method simple uses lems = (assumption | rule lems | standard)+
+method simple uses lem = (assumption | rule lem | standard)+
 
 
 subsection \<open>Wellformedness checker\<close>
 
-text "Find a proof of any valid typing judgment derivable from a given wellformed judgment.
-The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy."
+text "
+  \<open>wellformed\<close> finds a proof of any valid typing judgment derivable from the judgments passed as \<open>lem\<close>.
+  The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy.
+"
 
-method wellformed uses jdgmt declares wellform =
+method wellformed' uses jmt declares wellform =
   match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
-    catch \<open>rule rl[OF jdgmt]\<close> \<open>fail\<close> |
-    catch \<open>wellformed jdgmt: rl[OF jdgmt]\<close> \<open>fail\<close>
+    catch \<open>rule rl[OF jmt]\<close> \<open>fail\<close> |
+    catch \<open>wellformed' jmt: rl[OF jmt]\<close> \<open>fail\<close>
     )\<close>
 
+method wellformed uses lem =
+  match lem in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jmt: lem\<close>
 
-subsection \<open>Derivation search\<close>
-
-text "Combine \<open>simple\<close>, \<open>wellformed\<close> and the universe hierarchy rules to search for derivations of judgments.
-\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments.
-Definitions passed as \<open>unfolds\<close> are unfolded throughout."
-
-method derive uses lems unfolds = (
-  unfold unfolds |
-  simple lems: lems |
-  match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> |
-  rule U_hierarchy (*|
-  (rule U_cumulative, simple lems: lems) |
-  (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>)*)
-  )+
 
+subsection \<open>Derivation search\<close>
 
-subsection \<open>Simplification\<close>
+text " Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments."
 
-text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> search for lambda applications to simplify and are suitable for solving definitional equalities, as well as harder proofs where \<open>derive\<close> fails.
+method derive uses lem = (simple lem: lem | wellformed lem: lem)+
 
-It is however not true that these methods are strictly stronger; if they fail to find a suitable substitution they will fail where \<open>derive\<close> may succeed.
 
-\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules.
-In this case use \<open>rsimplify\<close> instead."
+subsection \<open>Substitution and simplification\<close>
 
-method rsimplify uses lems = (subst (0) comp, derive lems: lems)+
-  \<comment> \<open>\<open>subst\<close> performs an equational rewrite according to some computation rule declared as [comp], after which \<open>derive\<close> attempts to solve any new assumptions that arise.\<close>
+text "Import the \<open>subst\<close> method, used for substituting definitional equalities."
 
-method simplify uses lems = (simp add: lems | rsimplify lems: lems)+
+ML_file "~~/src/Tools/misc_legacy.ML"
+ML_file "~~/src/Tools/IsaPlanner/isand.ML"
+ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
+ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
+ML_file "~~/src/Tools/eqsubst.ML"
 
 
 end
\ No newline at end of file
diff --git a/Nat.thy b/Nat.thy
index eed9226..388df0f 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -42,8 +42,8 @@ and
     n: \<nat>
     \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)"
 
-lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
 lemmas Nat_intro = Nat_intro1 Nat_intro2
+lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2
 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
 
 
diff --git a/Proj.thy b/Proj.thy
index e90cd95..aa7e8ec 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -21,17 +21,14 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 
 lemma fst_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
-unfolding fst_def
-proof
-  show "A: U(i)" using assms(1) by (rule Sum_wellform)
-qed (fact assms | assumption)+
+unfolding fst_def by (derive lem: assms)
 
 
 lemma fst_comp:
   assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
 unfolding fst_def
 proof
-  show "\<And>x. x: A \<Longrightarrow> x: A" .
+  show "a: A" and "b: B(a)" by fact+
 qed (rule assms)+
 
 
@@ -39,20 +36,16 @@ lemma snd_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
 unfolding snd_def
 proof
-  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)"
-  proof -
-    have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type)
-    with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_wellform)
-  qed
-
+  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (derive lem: assms fst_type)
+  
   fix x y
   assume asm: "x: A" "y: B(x)"
   show "y: B(fst <x,y>)"
   proof (subst fst_comp)
-    show "A: U(i)" using assms(1) by (rule Sum_wellform)
-    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_wellform)
-  qed (rule asm)+
-qed (fact assms)
+    show "A: U(i)" by (wellformed lem: assms(1))
+    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" by (wellformed lem: assms(1))
+  qed fact+
+qed fact
 
 
 lemma snd_comp:
@@ -60,13 +53,12 @@ lemma snd_comp:
 unfolding snd_def
 proof
   show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
-  show "a: A" by (fact assms)
-  show "b: B(a)" by (fact assms)
-  show *: "B(a): U(i)" using assms(3) by (rule assms(2))
-  show "B(a): U(i)" by (fact *)
-qed
+  show "a: A" by fact
+  show "b: B(a)" by fact
+qed (simple lem: assms)
 
 
+lemmas Proj_types [intro] = fst_type snd_type
 lemmas Proj_comps [intro] = fst_comp snd_comp
 
 
diff --git a/ex/Methods.thy b/ex/Methods.thy
index d174dde..b0c5f92 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -1,6 +1,6 @@
 (*  Title:  HoTT/ex/Methods.thy
     Author: Josh Chen
-    Date:   Jul 2018
+    Date:   Aug 2018
 
 HoTT method usage examples
 *)
@@ -9,33 +9,40 @@ theory Methods
   imports "../HoTT"
 begin
 
+
 lemma
-  assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U"
-  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U"
-by (simple lems: assms)
+  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 (simple lem: assms)
 
 
 lemma
-  assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z"
+  assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)"
   shows
-    "A : U" and
-    "B: A \<rightarrow> U" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U"
+    "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" by (wellformed jdgmt: assms)
-  show "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
-  show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms)
-  show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms)
+  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 lem: assms)
 qed
 
 
-text "Typechecking:"
+text "Typechecking and constructing inhabitants:"
 
 \<comment> \<open>Correctly determines the type of the pair\<close>
-schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a, b) : ?A" by simple
-
-\<comment> \<open>Finds element\<close>
-schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple
+schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A"
+by simple
+
+\<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 assumption+
+done
 
 end
\ No newline at end of file