From 91efce41a2319a9fb861ff26d7dc8c49ec726d4c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 12 Jun 2018 12:30:54 +0200
Subject: Type rules now have \"all\" premises explicitly stated, matching the
 formulation in the HoTT book.

---
 Prod.thy | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 9ecab4d..113998e 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -1,5 +1,6 @@
 (*  Title:  HoTT/Prod.thy
     Author: Josh Chen
+    Date:   Jun 2018
 
 Dependent product (function) type for the HoTT logic.
 *)
@@ -10,8 +11,9 @@ theory Prod
 begin
 
 axiomatization
-  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  Prod :: "[Term, Typefam] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  \<comment> \<open>Application binds tighter than abstraction.\<close>
   appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
 
 syntax
@@ -29,15 +31,20 @@ translations
 
 \<comment> \<open>Type rules\<close>
 axiomatization where
-  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U"
+  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
 and
-  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)"
+  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
 and
-  Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)"
+  Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
-  Prod_comp [simp]: "\<And>A b a. a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
+  Prod_comp [simp]: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
 and
-  Prod_uniq [simp]: "\<And>A f. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq [simp]: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+
+\<comment> \<open>The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion.
+In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)".
+This forces the theorem prover to search for a suitable B. Is this additional overhead necessary?
+It *is* a safety check for well-formedness...\<close>
 
 text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
 
-- 
cgit v1.2.3