diff options
Diffstat (limited to 'Prod.thy')
| -rw-r--r-- | Prod.thy | 19 |
1 files changed, 13 insertions, 6 deletions
@@ -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)." |